# brixen/Epigram

added lambda calculus code to the manual

Showing with 43 additions and 0 deletions.
1. +43 −0 man/man.html
43 man/man.html
 @@ -400,6 +400,49 @@
+

Lambda Calculus

+

We can define the well-scoped lambda terms as an datatype indexed + by the number of varialbes it in scope. Any term of this type will + be guaranteed to be well-scoped, it will have no possibility of + dangling variables or unintended capture. We use the + type Fin again. This time to represent nameless + variables as de Bruijn indices:

+ +

> idata Fin : Nat -> Set := ('zero : (n : Nat) -> Fin ('suc + n)) ; ('suc : (n : Nat) -> Fin n -> Fin ('suc n)) ;

+ +

Before proceeding to define lambda terms we explain how to weaken + a renaming:

+ +

let wk (m : Nat)(n : Nat)(f : Fin m -> Fin n)(i : Fin ('suc + m)) : Fin ('suc n) ;
+ refine wk m n f i <= Fin.Ind ('suc m) i ;
+ refine wk m n f ('zero m) = 'zero n ;
+ refine wk m n f ('suc m i) = 'suc n (f i) ; +

+ +

The data type of lambda terms is defined as follow:

+ +

idata Lam : Nat -> Set := ('var : (n : Nat) -> Fin n -> Lam + n) ; ('app : (n : Nat) -> Lam n -> Lam n -> Lam n) ; ('lam : (n : + Nat) -> Lam ('suc n) -> Lam n) ;

+ +

Having defined lambda terms we define renaming:

+ + let ren (m : Nat)(n : Nat)(f : Fin m -> Fin n)(t : Lam m) + : Lam n ;
+ refine ren m n f t <= Lam.Ind m t ;
+ refine ren m n f ('var m i) = 'var n (f i) ;
+ refine ren m n f ('app m t u) = 'app n (ren m n f t) (ren m n f u) ;
+ refine ren m n f ('lam m t) = 'lam n (ren ('suc m) ('suc n) (wk m n f) + t) ; +

+ +

Unfortunately feeding the last line of this definition to Cochon + triggers a space leak at the time of writing

+ +
+

Appendix - List of Cochon commands

quit