I hereby claim:
- I am iwilare on github.
- I am iwilare (https://keybase.io/iwilare) on keybase.
- I have a public key ASDBYl3y4-9VLMf8M4sTLR57d97YndrcHh09apOae5rbuwo
To claim this, I am signing this object:
I hereby claim:
To claim this, I am signing this object:
E=([a,b],Γ=[])=>b?a?E(a,Γ)(E(b,Γ)):x=>E(b,[x,...Γ]):Γ[a] |
// 1-index De Bruijn, [0,n] abstraction, [f,x] application | |
let repr1 = [0, [[1, [0, [0, [0, [[3, 1], [2, 1]]]]]], [0, [0, 2]]]] | |
// 1-index De Bruijn, {f:, x:} application, {λ:} abstraction | |
let repr2 = {λ: {f: {f: 1, x: {λ: {λ: {λ: {f: {f: 3, x: 1}, x: {f: 2, x: 1}}}}}}, x: {λ: {λ: 2}}}} | |
// Named, {f:, x:} application, {λ:, b:} abstraction | |
let repr3 = {λ: 1, b: {f: {f: 1, x: {λ: 2, b: {λ: 3, b: {λ: 4, b: {f: {f: 2, x: 4}, x: {f: 3, x: 4}}}}}}, x: {λ: 2, b: {λ: 3, b: 2}}}} | |
// 0-index De Bruijn, {f:, x:} application, {λ:} abstraction | |
let reprN = {λ: {f: {f: 0, x: {λ: {λ: {λ: {f: {f: 2, x: 0}, x: {f: 1, x: 0}}}}}}, x: {λ: {λ: 1}}}} | |
// 0-index De Bruijn, {t:1, f:, x:} application, {t:0, λ:} abstraction | |
let repr4 = {t:0,λ: {t:1,f: {t:1,f: 0, x: {t:0,λ: {t:0,λ: {t:0,λ: {t:1,f: {t:1,f: 2, x: 0}, x: {t:1,f: 1, x: 0}}}}}}, x: {t:0,λ: {t:0,λ: 1}}}} |
data Lam | |
= Abs Lam | |
| App Lam Lam | |
| Var Int | |
data Stack = S [(Lam, Stack)] | |
krivine (App a b, S e, S s) = krivine (a, S e, S ((b, S e):s)) | |
krivine (Abs t, S e, S (c:s)) = krivine (t, S (c:e), S s) | |
krivine (Var n, S e, S s) = krivine (fst (e !! n), snd (e !! n), S s) |