nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpqkyagcdfagmkfyqwplpv0neng7nq24p4q3l4v7jhe3srlsmntufzs8tcpun (nprofile…cpun) nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpq26zlh0z0afh055uppfrtzhkkr824ya2p9wa3a2ghhj8ntfpnm7xqtulpgt (nprofile…lpgt) It is hard to find links to such things, though I'm sure they exist in abundance, but perhaps it would be helpful for me to briefly explain the idea in tweet form.
You want to index your types in natural numbers that describe how many variables are in the context. First, we should give a type of variables that can be made in a context of length "n". This is the type of de bruijn indices:
inductive Ix : Nat → Type where
| top : Ix (n+1)
| pop : Ix n → Ix (n+1)
So "top" means the rightmost in the context, and "pop x" means the variable that comes before "x". So the second-to-rightmost variable is "pop top".
Next, we define *terms* where variables are given by de bruijn indices. This starts off like this:
inductive Tm : Nat -> Type where
| var : Ix n -> Tm n
| lam : Tm (n+1) -> Tm n
| app : Tm n -> Tm n -> Tm n
...and so on. So you see that when you bind a variable, you increase the length of the context.
So then the term "\x.\y. x" is written: lam (lam (pop top)).
Does this help?
Jon Sterling /
npub1hf…9ls8k
2025-02-25 16:14:11
in reply to nevent1q…wpz0
Author Public Key
npub1hfga8wmley5fzqtttpeupd8hc6s92rykfmzktm8zfdhu9h8exvqsj9ls8kSeen on
wss://relay.mostr.pubPublished at
2025-02-25 16:14:11Event JSON
{
"id": "d04ce365c480fafe72d12316b2323e32d584578ceb6d49ea0b5012301abd9b0c",
"pubkey": "ba51d3bb7fc92891016b5873c0b4f7c6a0550c964ec565ece24b6fc2dcf93301",
"created_at": 1740500051,
"kind": 1,
"tags": [
[
"p",
"b13a8c353d46ec9201c1f858f9e668f4c0aa86a08feacf4af98c07f86e6be245",
"wss://relay.mostr.pub"
],
[
"p",
"5685fbbc4fea6efa53810a46b15ed619d55275412bbb1ea917bc8f35a433df8c",
"wss://relay.mostr.pub"
],
[
"p",
"ba0e1688a7414193a26f371924e606bbfef27833b13b83d4d81b376e3dcc8edf",
"wss://relay.mostr.pub"
],
[
"p",
"891a479d539158c59fe6fbaade872b07baf81f9dd6e9f0e9a9b5aced5a21fabe",
"wss://relay.mostr.pub"
],
[
"e",
"937066f4e8e5cd38d4b9097943c3d318166a28a38c7419cce5cdb7b5d870f601",
"wss://relay.mostr.pub",
"reply"
],
[
"proxy",
"https://mathstodon.xyz/users/jonmsterling/statuses/114065411350976639",
"activitypub"
]
],
"content": "nostr:nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpqkyagcdfagmkfyqwplpv0neng7nq24p4q3l4v7jhe3srlsmntufzs8tcpun nostr:nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpq26zlh0z0afh055uppfrtzhkkr824ya2p9wa3a2ghhj8ntfpnm7xqtulpgt It is hard to find links to such things, though I'm sure they exist in abundance, but perhaps it would be helpful for me to briefly explain the idea in tweet form.\n\nYou want to index your types in natural numbers that describe how many variables are in the context. First, we should give a type of variables that can be made in a context of length \"n\". This is the type of de bruijn indices:\n\ninductive Ix : Nat → Type where\n| top : Ix (n+1)\n| pop : Ix n → Ix (n+1)\n\nSo \"top\" means the rightmost in the context, and \"pop x\" means the variable that comes before \"x\". So the second-to-rightmost variable is \"pop top\". \n\nNext, we define *terms* where variables are given by de bruijn indices. This starts off like this:\n\ninductive Tm : Nat -\u003e Type where\n| var : Ix n -\u003e Tm n\n| lam : Tm (n+1) -\u003e Tm n\n| app : Tm n -\u003e Tm n -\u003e Tm n\n\n...and so on. So you see that when you bind a variable, you increase the length of the context.\n\nSo then the term \"\\x.\\y. x\" is written: lam (lam (pop top)).\n\nDoes this help?",
"sig": "11c7337ad994c511e7dd494b5639c10d2b17808949dfca36d5495e35e3bd4df1cbc8be054cb9ef6306ce291d5d4c9f91ea42d2ae3146b30726a06fa63af2f1ab"
}