; ; + - - - - - - - - - - - - - - - - - - - - - - - + ; | | ; | This is lacal.txt, a text file that contains | ; | the answers I, Savas Ali Tokmen, have | ; | prepared for the Lambda Calculus | ; | Assignment (CM20167) | ; | | ; + - - - - - - - - - - - - - - - - - - - - - - - + ; ; ; A copy of it normally should be found at the following address: ; ; http://people.bath.ac.uk/st221/CM20167/lacal.txt ; ; (Please make sure you directly download the text file, ; since the main folder is actually protected so you need ; a password to get a list of the files on that folder) ; ; It is organized in 2 parts: functions and tests ; - functions are divided in 3 parts: ; - the ones defined in the assesment questions, and some ; shortcuts to them (I'm lazy...) ; - the ones I have created (for greater comfort) ; - the answers to the assignment questions ; - testing includes tests for all these functions ; Quick note: if a function returns () [false], it very probably ; means that you've entered an argument that is not a variable, ; an abstraction or an application... Please note that those ; functions will * NOT * make any conversion between, for example: ; (a b c) => ((a b) c) ; (L (a b c) d) => (L a (L b (L c d))) ; etc. ; Basic functions... As seen on the instuctions sheet; note that the ; "abstraction?" function has been modified for greater reliability) ; Abstaction: lambda (L) var . body (defun mkabs (var body) (list 'L var body)) ; Variable of an abstaction (defun abs-var (a) (cadr a)) ; Body of an abstraction (defun abs-body (a) (caddr a)) ; Application: (m)(n) (defun mkapp (m n) (list m n)) ; Function of an application (defun app-fun (a) (car a)) ; Argument (or variable) of an application (defun app-arg (a) (cadr a)) ; Is a given thing a variable ? (defun variable? (l) (symbolp l)) ; Is a given thing an application ? (defun application? (l) (and (listp l) (= (length l) 2))) ; Is a given thing an abstraction ? ; *** WARNING *** code has been modified *** WARNING *** ; It now also checks that the list starts with a 'L (defun abstraction? (l) (and (listp l) (= (length l) 3) (eq (car l) 'L))) ; Handy shortcuts... I admit that I'm lazy ! (defun var? (x) (variable? x)) (defun app? (x) (application? x)) (defun abs? (x) (abstraction? x)) ; Other basic functions I'll be using... ; Replaces var1 with var2 in a given list and on all its sublists ; by browsing the list until it finds atoms and when it does ; compares the atom with var1, if same then returns var2 ; A small modification has been made to make it act good with ; applications, abstractions and alpha renaming (mostly not to ; overwrite the 'L symbol in the beginning of an abstraction, and ; also to alpha-rename all sub-abstractions that use var1 as variable) (defun rplc (inList var1 var2) (if (listp inList) ; inList is a list: do a recursion (if (eq () inList) () (if (abs? inList) ; inList is an abstraction... be careful! (if (eq (abs-var inList) var1) ; var1 is the same as the sub-abstraction variable, ; a new alpha-renaming is therefore required for ; this sub-abstraction... (arename inList var1 (gensym)) ; var1 is still bound... keep on replacing... (mkabs (rplc (abs-var inList) var1 var2) (rplc (abs-body inList) var1 var2))) ; not an abstraction... replace "stupidly" (cons (rplc (car inList) var1 var2) (rplc (cdr inList) var1 var2)))) ; inList is not a list: compare with var1 (if (eq inList var1) var2 inList))) ; Tells you if an element is in a lambda-term ; Simply browses the term, until its atoms, and then compares the ; atom with the needle (defun in_lambda (haystack needle) (if (listp haystack) ; haystack is a list... (if (eq haystack ()) ; the list is empty, therefore cannot contain needle () (if (listp (car haystack)) ; first element of list is a list; ; therefore an abstraction or application (if (abs? (car haystack)) ; first element of list is an abstraction ; search the variable & body (or (eq (abs-var (car haystack)) needle) (in_lambda (abs-body (car haystack)) needle)) ; first element of list is an application ; search both terms one by one (or (in_lambda (app-fun (car haystack)) needle) (in_lambda (app-arg (car haystack)) needle))) ; first element of list is atom... (if (eq (car haystack) needle) ; found it! #t ; did not find it, keep searching (in_lambda (cdr haystack) needle)))) ; haystack is an atom: compare it with the needle (eq haystack needle))) ; Tells you a list of atoms is present in another list of atoms, ; by doing a loop on both arguments (defun in_list (haystack needle) (if (eq needle ()) ; the empty list is contained in everything #t (if (eq haystack ()) ; the empty list doesn't contain anything () (if (or (atom needle) (atom haystack)) ; needle or haystack are atoms... that's actually ; * AGAINST * the specification but can be caused ; by one of the recursive calls... so is normal (equal needle haystack) ; compare... (or (and ; it starts the same... (equal (car needle) (car haystack)) ; let's see if it also ends the same (in_list (cdr haystack) (cdr needle))) ; it doesn't start the same... keep on searching! (in_list (cdr haystack) needle) (in_list (car haystack) needle)))))) ; Tells you if a part of a list of lists of atoms is present in a ; list of atoms (uses the in_list function defined above, and the ; "_r" just means that it does a recursion on the haystack) (defun in_list_r (haystack needle) (if (eq haystack ()) ; the empty list doesn't contain anything () ; compare... (or ; is it in the first element? (in_list needle (car haystack)) ; or in the rest? (in_list_r (cdr haystack) needle)))) ; Now ... the wanted functions ! ; *** Alpha renaming *** ; ; HOW ALPHA RENAMING WORKS ; We actually do it for the 3 cases: ; - if the term is a variable, it means that it is by definition ; free. So, it is NOT renamed and since it is a variable no ; recursion needs to be done (1) ; - if the term is an application, it means that we should apply ; the renaming to its two elements (2) ; - if the term is an abstraction, we should check its argument: ; - if the argument is equal to var1, replace all ; occurences of var1 with var2 in the body (3) ; - apply the alpha-renaming function to the body ; otherwise... And not touch the argument! (4) (defun arename (term var1 var2) ; check for name captures... (if (in_lambda term var2) ; name capture! change var2 (setq var2 (gensym))) (cond ; case (1) ((var? term) term) ; case (2) ((app? term) (mkapp (arename (app-fun term) var1 var2) (arename (app-arg term) var1 var2))) ; Term is an abstraction... Now gets interesting! ((abs? term) (if (eq (abs-var term) var1) ; case (3) (mkabs var2 (rplc (abs-body term) var1 var2)) ; case (4) (mkabs (abs-var term) (arename (abs-body term) var1 var2)))))) ; *** Lambda-term substitution *** ; HOW LAMBDA-TERM SUBSTITUTION WORKS ; We do it for the 3 cases: ; - if the term is a variable, then this means it is by definition ; free. We therefore check if it is equal to the given x, and ; if it is the case replace (1) ; - if the term is an application, it means that we should apply ; the substitution to its two elements (2) ; - if the term is an abstraction, we should check for nameclashes ; and then substitute in the the abstraction body (3) (defun subst (M x N) (cond ; case (1) ((var? M) ; check if M equals x (for a variable) (if (eq M x) ; yes it is... return N N ; no... keep as is M)) ; case (2) ((app? M) (mkapp (subst (app-fun M) x N) (subst (app-arg M) x N))) ; case (3) ((abs? M) ; check whether x is free or bound (if (eq (abs-var M) x) ; x is bound! stop M ; x is not bound... check for name clashes (if (in_lambda (list N) (abs-var M)) ; nameclash: N contains the abstraction's variable ; in a non-bound way... we should therefore do ; an alpha-renaming before proceeding (subst (arename M (abs-var M) (gensym)) x N) ; we have no problem... substitute as is (mkabs (abs-var M) (subst (abs-body M) x N))))))) ; *** Beta reduction *** ; HOW BETA REDUCTION WORKS ; We do it for the 3 cases: ; - if the term is a variable, it doesn't touch anything (1) ; - if the term is and application: ; - if the first term is a lambda, then does a substitution (2) ; - otherwise, keeps on "digging deeper" (3) ; - if the term is an abstraction, it does a beta-reduction ; on its body (4) ; And, some word about the stopping heuristic: the function keeps a ; history (=list) of the past results, and at every step checks if ; the current step is not a part of one of the old steps. If it is, ; then this means that we have a self-duplicating code (or that the ; reduction is finished) so we should stop. This is probably one of ; the slowest, yet in my opinion quite effective heuristic. ; Since the function uses the subst function defined before, name ; clash and capture handling will be done by the subst function... ; This is the function that holds the stopping heuristics... ; It actually is called with the term to beta-reduce and with a list ; of past actions (history). It calls the main beta reduction function, ; and then verifies that the result is not in the history. If the ; result is not in the history, then is keeps on trying to beta-reduce ; more. Otherwise, well... It stops! (defun beta_reduce (term history) (if (in_list_r history term) ; this is where the function says "hey.. I've seen that before!" term ; never seen that before... keep on searching... (beta_reduce (beta_reduce_main term) (cons term history)))) ; This is the "main" beta-reduction function, as described above (defun beta_reduce_main (term) (cond ; case (1) ((var? term) term) ; case (2) ((app? term) (cond ; case (3), with first term a variable ((var? (app-fun term)) (mkapp (app-fun term) (beta_reduce_main (app-arg term)))) ; case (3), with first term an application ((app? (app-fun term)) (mkapp (beta_reduce_main (app-fun term)) (beta_reduce_main (app-arg term)))) ; case (2) ((abs? (app-fun term)) (subst (abs-body (app-fun term)) (abs-var (app-fun term)) (app-arg term))))) ; case (4) ((abs? term) (mkabs (abs-var term) (beta_reduce_main (abs-body term)))))) ; And... The beta reduction function. ; Since we are at the beginning when starting, beta is actually the ; same as calling beta_reduce without any (= an empty) history... (defun beta (term) (beta_reduce term ())) ; And ... testing ! ; *** Make application & abstraction *** ; ; (mkapp 'a 'b) ; ;> (a b) ; (mkabs 'a 'b) ; ;> (L a b) ; ; (var? 'a) ; ;> #t ; (var? '(a)) ; ;> () ; ; *** Is application ? *** ; ; (app? 'a) ; ;> () ; (app? '(a)) ; ;> () ; (app? '(a b)) ; ;> #t ; (app? '((a) (b))) ; ;> #t ; (app? '(a b c)) ; ;> () ; ; *** Is abstraction ? *** ; ; (abs? 'a) ; ;> () ; (abs? '(a)) ; ;> () ; (abs? '(a b)) ; ;> () ; (abs? '(a b c)) ; ;> () ; (abs? '(L b c)) ; ;> #t ; (abs? '(a b c d)) ; ;> () ; (abs? '(L a b c)) ; ;> () ; (abs? '(L a (b c))) ; ;> #t ; ; *** "replace" function *** ; ; (rplc 'a 'a 'b) ; ;> b ; (rplc 'a 'b 'c) ; ;> a ; (rplc ; '(t (h) e ; (q u i (c k)) ; b r (o w n (f o)) x ; j (u m) p s ; (o v) e r ; (t h e) ; l a (z (y ; (d (o))) g)) ; 'o 'q) ; ;> (t (h) e ; (q u i (c k)) ; b r (q w n ; (f q)) x ; j (u m) p s ; (q v) e r ; (t h e) ; l a (z (y ; (d (q))) g)) ; (rplc '(x (L y (x (L x (x x))))) 'x 'w) ; ;> (w (L y (w (L z (z z))))) ; (rplc '(x (L y (x (L x ((q x) q))))) 'q 'w) ; ;> (x (L y (x (L x ((w x) w))))) ; ; *** "in_lambda" function *** ; ; (in_lambda 'a 'a) ; ;> #t ; (in_lambda '(a b) 'a) ; ;> #t ; (in_lambda '(a b) 'c) ; ;> () ; (in_lambda '(( L x ((x y) z)) (a (L a (b c)))) 'x) ; ;> #t ; (in_lambda '(( L x ((x y) z)) (a (L a (b c)))) 'y) ; ;> #t ; (in_lambda '(( L x ((x y) z)) (a (L a (b c)))) 'L) ; ;> () ; (in_lambda '(( L x ((x L) z)) (a (L a (b c)))) 'L) ; ;> #t ; ; *** "in_list" function *** ; ; (in_list 'a 'a) ; ;> #t ; (in_list 'a 'b) ; ;> () ; (in_list '(a b c d) 'b) ; ;> () ; (in_list '(a b c d) '(b)) ; ;> #t ; (in_list '(a b c (d e f (g h (i j k (l m n)) o p) q r) s t v) ; '(m)) ; ;> #t ; (in_list '(a b c (d e f (g h (i j k (l m n)) o p) q r) s t v) ; '(l m)) ; ;> #t ; (in_list '(a b c (d e f (g h (i j k (l m n)) o p) q r) s t v) ; '(j k (l m n))) ; ;> #t ; (in_list '(a b c (d e f (g h (i j k (l m n)) o p) q r) s t v) ; '(j k (m))) ; ;> () ; ; *** "in_list_r" function *** ; (tests taken directly from ; beta reductions) ; ; (in_list_r ; '(((L x (P x)) j) ; (((L Q (L x (Q x))) P) j) ; ((L G9 (((L Q (L x (Q x))) P) G9)) j) ; (((L G8 (L G9 (((L Q (L x (Q x))) G8) G9))) P) j) ; ((((L GQ (L L (L x ((GQ L) x)))) (L Q (L x (Q x)))) P) j)) ; '(P j)) ; ;> () ; (in_list_r ; '(((L x (L y (L z (((x x) y) z)))) ; (L x (L y (L z (((x x) y) z)))))) ; '(L G10 (L G11 ((((L x (L y (L z (((x x) y) z)))) ; (L x (L y (L z (((x x) y) z))))) G10) G11)))) ; ;> #t ; ; *** Alpha renaming *** ; ; (arename 'x 'x 'a) ; ;> x ; (arename '(x y) 'x 'a) ; ;> (x y) ; (arename '(L x x) 'x 'b) ; ;> (L b b) ; (arename '(L y y) 'x 'b) ; ;> (L y y) ; (arename '(L x y) 'x 'b) ; ;> (L b y) ; (arename '(L y x) 'x 'b) ; ;> (L y x) ; (arename '(L x (x y)) 'x 'y) ; ;> (L z (z y)) ; (arename '(L x (L x (x x))) 'x 'y) ; ;> (L y (L z (z z))) ; (arename '(L x (x (L x (x y)))) 'x 'y) ; ;> (L z (z (L w (w y)))) ; (arename '(L x (L y ((x y) z))) 'x 'y) ; ;> (L w (L y ((w y) z))) ; (arename '(L y (x y)) 'x 'y) ; ;> (L y (x y)) ; (arename '(L y (x y)) 'y 'x) ; ;> (L z (x z)) ; (arename '((x y) (L x (x a))) 'x 'a) ; ;> ((x y) (L z (z a))) ; (arename '((x a) (L x (x y))) 'x 'a) ; ;> ((x a) (L z (z y))) ; (arename '(((x y) (L x (x a))) ((x y) (L x (x a)))) 'x 'a) ; ;> (((x y) (L z (z a))) ((x y) (L z (z a)))) ; (arename '(((x y) (L x (x a))) ((x y) (L x (x b)))) 'x 'a) ; ;> (((x y) (L z (z a))) ((x y) (L z (z b)))) ; ; *** Substitution *** ; ; (subst 'a 'a 'b) ; ;> b ; (subst 'a 'b 'c) ; ;> a ; (subst '(a b) 'a 'c) ; ;> (c b) ; (subst 'x 'x '(L y y)) ; ;> (L y y) ; (subst '(L x (x y)) 'x '(L z (z z))) ; ;> (L x (x y)) ; (subst '(L x (x y)) 'y '(L z (z z))) ; ;> (L x (x (L z (z z)))) ; ; test with full alpha renaming ; (subst '(L x (x y)) 'y '(L x (x x))) ; ;> (L w (w (L x (x x)))) ; ; test with partial alpha renaming ; (subst '((L x (x y)) (L w (w y))) 'y '(L x (x x))) ; ;> ((L q (q (L x (x x)))) (L w (w (L x (x x))))) ; ; *** Beta reduction *** ; ; (beta '((L x y) z)) ; ;> y ; (beta '(x (((L x (x y)) z) y))) ; ;> (x ((z y) y)) ; (beta '((L x (x y)) (L z (z z)))) ; ;> (y y) ; (beta '((x (L y y)) z)) ; ;> ((x (L y y)) z)) ; (beta '((L z (L x (x y))) x)) ; ;> (L a (a y)) ; (beta '(L x ((L y (x y)) z))) ; ;> (L x (x z)) ; (beta '((L x (x x)) (L x (x y)))) ; ;> (y y) ; (beta '((L x (x (x x))) (L x (x y)))) ; ;> (y y y) ; ; ; LOOP TESTS ("OM" stands for "Omega") ; ; (beta OM*) should normally be intelligent enough to stop by itself ; ; for most of the looping reductions... ; ; ; simple loop test ; (setq OM0 '(L x (x x))) ; (beta (mkapp OM0 OM0)) ; ;> ((L x (x x)) (L x (x x))) ; ; ; expanding loop test ; (setq OM1 '(L x ((x x) x))) ; (beta (mkapp OM1 OM1)) ; ;> [...] (L x ((x x) x))) [...] ; ; ; loop in 2 steps ; (setq OM2 '(L x (L y ((y x) y)))) ; (beta (mkapp OM2 OM2)) ; ;> [...] (L x (L y ((x x) y)))) [...] ; ; ; loop in 3 steps ; (setq OM3 '(L x (L y (L z (((z x) y) z))))) ; (beta (mkapp OM3 OM3)) ; ;> [...] (L x (L y (L z (((x x) y) z))))) [...] ; ; ; Test cases taken from http://ling.ucsd.edu/~barker/Lambda/ ; ; What I've actually done is that I've compared the results ; ; of my program with the ones of the site's examples ; ; (beta '((L x (it x)) works)) ; ;> (it works) ; (beta '((L x (L y1 (x y1))) z)) ; ;> (L y1 (z y1)) ; (beta '((L x (L y (x y))) y)) ; ;> (L y1 (y y1)) ; (beta '((L x (x x))(L x (L y (x y))))) ; ;> (L y1 (L y2 (y1 y2))) ; (beta '(L x (P x))) ; ;> (L x (P x)) ; (beta '((L x ((x y) z)) z)) ; ;> (z y z) ; (beta '((L x (w y)) z)) ; ;> (w y) ; (beta '((L x (P x)) j)) ; ;> (P j) ; (beta '(((L x (L y (P y))) j) m)) ; ;> (P m) ; (beta '(((L y (L x ((K x) y))) j) m)) ; ;> (K m j) ; (beta '(((L Q (L x (Q x))) (L y (P y))) j)) ; ;> (P j) ; (beta '( ; (((L GQ (L L (L x ((GQ L) x)))) ; (L Q (L x (Q x)))) P) j)) ; ;> (P j) ; (beta '((L x ((L x ((K x) x)) j)) m)) ; ;> (K j j) ; ; ; ; + - - - - - - - - - - - - - - - - - - - - - - - + ; | | ; | To contact me, please see | ; | http://people.bath.ac.uk/st221/ | ; | | ; | This point marks the end of this document | ; | | ; + - - - - - - - - - - - - - - - - - - - - - - - + ;