;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;                                                                                ;
;       Lambda Calculus Implementation In EuLisp                                 ;
;       Natalie Downe (cs1njd@bath.ac.uk)                                        ;
;                                                                                ;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


; 1. function l-term - represents a data structure used to display a lambda term in a standard manner.
; (Supports all)
; DESCRIPTION: takes 2 or more arguments which can be either symbols or listsit returns the lambda term in my l-term data structure i.e. lambda xy.z is (l-term (x) (l-term (y) (z))) If the 1st argument is a list of length 1 it returns a list'l-term and the arg with the rest of the list given to the function flattened (all but 1 outer set of brackets, removed)if the list has length of more than one, it returns the above for the first one then reccursively callsitself on the next term in the list. If however arg is not a list it is a symbol, so the function creates a list of the 'l-term with the arg as a list and the flattened retn list. If by mistake you were to try and enter L().x the function would assume you meant to enter a symbol

(defun l-term (arg . retn)
    (if (eq arg ())
        (flattenList retn)
        (if (listp arg)
            (if (= 1 (length arg))
                (list 'l-term (flattenList arg) (flattenList retn))
                (list 'l-term (list (car (flattenList arg))) (l-term (cdr (flattenList arg)) (flattenList retn)))
            )
            (list 'l-term (flattenList (list arg)) (flattenList retn))
        )
    )
)



; 2. function flattenList - squashes a list with many sublists, into one list. 
; (Supports fn 1. fn 3. fn 4.)
; DESCRIPTION: takes a list which can have many sublists returns the empty list if the listGiven is an empty list, else (if true)calls itself reccursively and returns the original list in just one set of outer parenthesis.

(defun flattenList (listGiven)
    (cond 
        ((null listGiven) ())
        ((atom listGiven) (list listGiven))
        (t (append (flattenList (car listGiven))
            (flattenList (cdr listGiven)))
        )
    )
)



; 3. function boundVar - takes a lambda term and returns a list of all the bound variables.
; (Supports fn 8.)
; DESCRIPTION: if it is anything but a lambda term (ie a symbol) then it returns the empty list because variables are free. 

(defun boundVar (givenTerm)
    (if (listp givenTerm)
        (if (eq (car givenTerm) 'l-term)
            (flattenList (cons (cadr givenTerm) (boundVar (car (cdr (cdr givenTerm))))))
            ()
        )
        ()
    )
)



; 4. function retnVar - takes a lambda term and returns a list of the variables that that function returns.
; (Supports fn 8.) 
; DESCRIPTION: Cycles through the given term when it is in the proper data structure till it finds the list of values at the end, which the lambda term returns.

(defun retnVar (givenTerm)
    (if (listp givenTerm)
        (if (eq (car givenTerm) 'l-term)
            (retnVar (car (cdr (cdr givenTerm))))
            (flattenList givenTerm)
        )
        (list givenTerm)
     )
)



; 5. function is-in - takes two lists checks if an atom in lst is in var, returns true or false.
; (Supports fn 6.)
; DESCRIPTION: If lst is empty the function returns the empty list, if it is not in empty it checks if the two lists are the same and if so returns true. if the two lists are not equal calls itself again on itself minus the 1st element.

(defun is-in (var lst)
    (if (eq () lst)
        ()
        (if (eq var (car lst))
            t
            (is-in var (cdr lst))
         )
     )
)



; 6. function removeVar - again takes two lists, and performs is-in, on them, all variables in the 1st that are also in the second, are removed from the 2nd, this is then returned.
; (Supports fn 8.)
; DESCRIPTION: various conditionals are performed upon the two inputs, to ensure that the right arguments are sent to opperations such as car and cdr ect. The main bit of the code is only excicted if both var and lst are lists and lst is of length greater than zero. if the list is greater than length zero, and the first element of lst is in var it calls itself using (var) and (lst minus the top element), if it is not in var it checks the next element.

(defun removeVar (list1 list2)
    (if (listp list1)
        (if (listp list2)
            (if (> (length list2) 0)
                (if (is-in (car list2) list1)
                    (removeVar list1 (cdr list2))
                    (cons (car list2) (removeVar list1 (cdr list2)))
                 )
                ()
            )
            (if (is-in list2 list1)
                ()
                (list list2)
            )
        )
        (removeVar (list list1) list2)
    )
)



; 7. function removeDuplicates - take a list and goes through it reccursively, returns a list with no duplicates.
; (Supports fn 8. fn 3.) 
; DESCRIPTION: if the 1st item in a given list is found to exist in the rest of the list, the remove duplicates function is called on the remaining items (the tail of the list) disregarding the repeated item at the begining of the list. if however the 1at item in the given list is not duplicated, that item is kept and the function removeduplicates is called upon the rest of the list.

(defun removeDuplicates (givenList)
    (if (eq givenList ())
        ()
        (if (is-in (car givenList) (cdr givenList))
            (removeDuplicates (cdr givenList))
            (cons (car givenList) (removeDuplicates (cdr givenList)))
        )
    )
)

; 8. function freeVar - takes a lambda term and returns a list of all the variables in the lambda term which are free.
; (Supports fn.)
; DESCRIPTION: calls removeVar with the arguments as the list of all the bound variables in givenTerm and the variables which the lambda term returns. if a variable appears in the latter and not in the former then it is classed as 'free'

(defun freeVar (givenTerm)
    (removeDuplicates (removeVar (boundVar givenTerm) (retnVar givenTerm)))
)



; 9. function makeApp - make application, M and N must be lambda terms
; (Supports fn.)
; DESCRIPTION: constructs a list of two lambda terms as an application.

(defun makeApp (M N)
    (list (list M) (list N))
)



; 10. function getFirstTerm - deconstuct application gets the first term of the application.
;(Supports fn.)
; DESCRIPTION: gets the first term of an application by using car - which returns first item of the list.

(defun getFirstTerm (application)
    (car application)
)



; 11. function getLastTerm - deconstuct application gets the last term of the application.
; (Supports fn.)
; DESCRIPTION: gets the last term of a two term application by using cdr - which returns the list minus the 1st item.

(defun getLastTerm (application)
    (cdr application)
)



; 12 function replaceVar - takes a list and two variables, retuns a list with all instances of the 1st variable (var1), replaced with the second (var2).
; (Supports fn 13.)
; DESCRIPTION: replaces all instance of the first variable in the list with the second symbol. 

(defun replaceVar (var1 var2 listGiven)
    (if (listp listGiven)
        (if (eq () listGiven)
            ()
            (cons (replaceVar var1 var2 (car listGiven)) (replaceVar var1 var2 (cdr listGiven)))
        )
        (if (symbolp listGiven) 
            (if (eq listGiven var1)
                var2
                listGiven
            )
        )
    )
)



; 13. function replaceVar2 - Takes a symbol and a list, returns a list with all instances of the variable in the list 
; replaced with a general symbol.
; (Supports fn 14.)
; DESCRIPTION: Very similar to replaceVar only it takes 2 arguments, a list and one variable. It calls the function replaceVar using the 1st argument it was given as var1, the second argument (the list) as listGiven. It then uses athe lisp general symbol function gensym as what it should replace it with. 

(defun replaceVar2 (var1 listGiven)
    (replaceVar var1 (gensym) listGiven)    
)



; 14. function alphaRename - ALPHA RENAMING - takes a lambda term and 2 variables, returns a lambda term
; (Supports fn 15.)
; DESCRIPTION: Only renames the bound variables in the lambda term. Uses  the pre defined replaceVar function if there is no danger of transforming a free variable to be bound. if however there is a free variable with the same name as the variable due to be replaced with then the function replaceVar2 needs to be called, replacing all occurances of var 1 in termGiven with a general symbol.

(defun alphaRename (var1 var2 termGiven)
    (if (is-in var1 (boundVar termGiven))
        ; change the lambda term into a list replaceVar rename bound and 
        ; return variables
        (if (is-in var2 (freeVar termGiven))
            (l-term (flattenList (replaceVar2 var1 (boundVar termGiven))) (flattenList (replaceVar2 var1 (retnVar termGiven)))) ; *
            (l-term (flattenList (replaceVar var1 var2 (boundVar termGiven))) (flattenList (replaceVar var1 var2 (retnVar termGiven))))
        )
        termGiven
    )
    
)

; Unfortunatly because the function replaceVar2 is called twice (on the 1st item and then on the rest) in line * two different general symbols appear. 
; (See testing.)

; Also I was unsure whether it was allowed, to alpha rename a term such as Lxy.xy renaming x with y. At present my code allows this as what it is replacing is a bound variable. There should really be a test to check whether var2 is a bound variable in the term, if it is there should be use of the function replaceVar2.



; 15. function substitute - SUBSTITUTION - function to perform substitution with a lambda expression. Takes two single lambda terms and a variable returns a lambda term with all occurances of the variable replaced with 
; the first lambda term. 
; (Supports fn 16.)
; DESCRIPTION: This function implements the definition of substitution.

(defun substitute (expr1 var expr2)
    (cond
        ((symbolp expr2)
            (if (eq var expr2)
                expr1
                expr2
            )
        )
        ((listp expr2)
            (cond
                ((eq (length expr2) 0) ; null
                    ()
                )
                ((eq (length expr2) 2) ; application
                    (makeApp (substitute expr1 var (getFirstTerm expr2)) (substitute expr1 var (getLastTerm expr2)))
                )
                ((eq (length expr2) 1)
                ; if abstsaction but var bound return abstsaction
                    (if (eq (car expr2) 'l-term)
                        ; if abstraction do this:
                        (if (or (is-in (cadr expr2) (boundVar expr1)) (is-in var (retnVar expr2)))
                            (l-term (flattenList (boundVar expr2)) (flattenList (substitute expr1 var (freeVar expr2))))  
                            (if (and (is-in (cadr expr2) (boundVar expr1)) (is-in var (retnVar expr2)))
                                (alphaRename var expr1 (l-term (flattenList (boundVar expr2)) (flattenList (substitute expr1 var (freeVar expr2)))))
                            )
                        )
                        ; if not an abstraction, do this:
                        (replaceVar var expr1 expr2)
                    )
                )
                ((> (length expr2) 2)
                    (if (eq (car expr2) 'l-term)
                        (cons (substitute expr1 var (car expr2)) (substitute expr1 var (cdr expr2)))
                        (replaceVar var expr1 expr2)
                    )
                )
            )
        )
    )
)



; 17. function betaReduce - function to perform beta reduction. Takes an expression and returns what the lambda function ; returns.
; DESCRIPTION: This function implements the definition of beta reduction.

(defun betaReduce (expression)
    (cond
        ((not (listp expression)) 
            expression
        )
        (t ; expression is a list
           (cond 
                ((eq (length expression) 0)
                    () ; null argument
                )
                ((eq (length expression) 1)
                    expression ; it could be an atom, a list or an abstraction
                )
                ((eq (length expression) 2)
                    ;1st on is a lamda term do reccursion on each bit and make app 
                    (substitute (gensym) (car expression) (cadr expression))
                )
                (t ; list of length greater than 2
                    (cons (betaReduce (car expression)) (betaReduce (cadr expression)))
                )
            )
        )
    )
)

; should (Lxy.xyz)(Lpq.p)(Lie.u) equal...

; ((Lxy.xyz))(Lpq.p)(Lie.u))
; (L(Lpq.p)(Lie.u).(Lpq.p)(Lie.u)z) ; because (Lxy.xyz) takes 2 arguments

; or

; (((Lxy.xyz)(Lpq.p))(Lie.u)) ; because lambda terms left associate
; (L(Lpq.p)y.(Lpq.p)yz)(Lie.u)
; (L(L(Lie.u)q.(Lie.u))y.(L(Lie.u)q.(Lie.u))yz)
; (((Lie.u)q.(Lie.u))y.(L(Lie.u)q.(Lie.u))yz)
; My code supports this view