Skip to content

Commit

Permalink
Lambda Reducer
Browse files Browse the repository at this point in the history 
Implements recursive beta-reduction of Lambda terms alongside several
arithmetic/predicate optimizations.
  • Loading branch information
@agureev @mariari
agureev authored and mariari committed Oct 11, 2023
1 parent 7bd72f6 commit 06b05b7
Show file tree
Hide file tree
Showing 5 changed files with 332 additions and 80 deletions.
311 changes: 311 additions & 0 deletions src/lambda/lambda.lisp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -397,3 +397,314 @@ nil"))
(or (errorp (ltm tterm))
(errorp (rtm tterm))))
(t (errorp (term tterm)))))

(defun dispatch (tterm)
"A dispatch refering the class of a term to its function"
(typecase tterm
(absurd #'absurd)
(unit #'unit)
(left #'left)
(right #'right)
(case-on #'case-on)
(fst #'fst)
(snd #'snd)
(pair #'pair)
(lamb #'lamb)
(app #'app)
(index #'index)
(err #'err)
(bit-choice #'bit-choice)
(plus #'plus)
(minus #'minus)
(divide #'divide)
(times #'times)
(lamb-eq #'lamb-eq)
(lamb-lt #'lamb-lt)
(modulo #'modulo)))

(defun dispatch-arith (tterm)
"A dispatch refering the class of an arithmetic term
to its corresponding operation"
(typecase tterm
(plus #'+)
(minus #'-)
(divide #'floor)
(times #'*)
(lamb-eq #'=)
(lamb-lt #'<)
(modulo #'mod)))

(defun index-excess (tterm)
"Checks all indeces occuring in a term which will be substituted.
If position exceeds n, adds depth to the index. Necessary for
beta-substitution of indices which point outside of the app term"
(labels ((rec (n tterm)
(typecase tterm
(absurd (absurd (tcod tterm)
(rec n (term tterm))))
(left (left (rty tterm)
(rec n (term tterm))))
(right (right (lty tterm)
(rec n (term tterm))))
(case-on (case-on (rec n (on tterm))
(rec (1+ n) (ltm tterm))
(rec (1+ n) (rtm tterm))))
(fst (fst (rec n (term tterm))))
(snd (snd (rec n (term tterm))))
(lamb (lamb (tdom tterm)
(rec (1+ n) (term tterm))))
(app (app (rec n (fun tterm))
(list (rec n (car (term tterm))))))
(index (if (>= (pos tterm) n)
(index (1+ (pos tterm)))
tterm))
((or unit
err
bit-choice)
tterm)
((or plus
times
minus
divide
lamb-eq
lamb-lt
pair
modulo)
(funcall (dispatch tterm)
(rec n (ltm tterm))
(rec n (rtm tterm)))))))
(rec 0 tterm)))

(defun index-lack (n tterm)
"Checks if a term has made substitutions and decreases the index
of term accordingly"
(labels ((rec (n tterm)
(if (typep tterm 'list)
tterm
(typecase tterm
(absurd (absurd (tcod tterm)
(rec n (term tterm))))
(left (left (rty tterm)
(rec n (term tterm))))
(right (right (lty tterm)
(rec n (term tterm))))
(case-on (case-on (rec n (on tterm))
(rec (1+ n) (ltm tterm))
(rec (1+ n) (rtm tterm))))
(fst (fst (rec n (term tterm))))
(snd (snd (rec n (term tterm))))
(lamb (lamb (tdom tterm)
(rec (1+ n) (term tterm))))
(app (app (rec n (fun tterm))
(list (rec n (car (term tterm))))))
(index (if (> (pos tterm) n)
(index (1- (pos tterm)))
tterm))
((or unit
err
bit-choice)
tterm)
((or plus
times
minus
divide
lamb-eq
lamb-lt
pair
modulo)
(funcall (dispatch tterm)
(rec n (ltm tterm))
(rec n (rtm tterm))))))))
(rec n tterm)))

(defun delist (tterm)
"We mark substituted terms by listing them. This function recovers the car
of the list."
(if (typep tterm 'list)
(car tterm)
(typecase tterm
(absurd (absurd (tcod tterm)
(delist (term tterm))))
(left (left (rty tterm)
(delist (term tterm))))
(right (right (lty tterm)
(delist (term tterm))))
(case-on (case-on (delist (on tterm))
(delist (ltm tterm))
(delist (rtm tterm))))
(fst (fst (delist (term tterm))))
(snd (snd (delist (term tterm))))
(lamb (lamb (tdom tterm)
(delist (term tterm))))
(app (app (delist (fun tterm))
(list (delist (car (term tterm))))))
((or unit
err
index
bit-choice)
tterm)
((or plus
times
minus
divide
lamb-eq
lamb-lt
pair
modulo)
(funcall (dispatch tterm)
(delist (ltm tterm))
(delist (rtm tterm)))))))

(defun sub (ind term-to-replace sub-in)
"Substitutes the occurence of index (ind) inside of the top
subterms of sub-on by term-to-replace. We mark replaced terms by
listing them"
(typecase sub-in
(absurd (absurd (tcod sub-in) (sub ind
term-to-replace
(term sub-in))))
(left (left (rty sub-in) (sub ind
term-to-replace
(term sub-in))))
(right (right (lty sub-in) (sub ind
term-to-replace
(term sub-in))))
(case-on (case-on (sub ind
term-to-replace
(on sub-in))
(sub (1+ ind)
(index-excess term-to-replace)
(ltm sub-in))
(sub (1+ ind)
(index-excess term-to-replace)
(rtm sub-in))))
(fst (fst (substitute ind
term-to-replace
(term sub-in))))
(snd (snd (substitute ind
term-to-replace
(term sub-in))))
(lamb (lamb (tdom sub-in)
(sub (1+ ind)
(index-excess term-to-replace)
(term sub-in))))
(app (app (sub ind term-to-replace (fun sub-in))
(list (sub ind term-to-replace (car (term sub-in))))))
(index (if (= (pos sub-in) ind)
(list term-to-replace)
sub-in))
((or unit
err
bit-choice)
sub-in)
((or plus
times
minus
divide
lamb-eq
lamb-lt
pair
modulo)
(funcall (dispatch sub-in)
(sub ind term-to-replace (ltm sub-in))
(sub ind term-to-replace (rtm sub-in))))))

(defun reducer (tterm)
"Reduces a given Lambda term by applying explict beta-reduction
when possible alongside arithmetic simplification. We assume that the
lambda and app terms are 1-argument"
(typecase tterm
(absurd (absurd (tcod tterm) (reducer (term tterm))))
(left (left (rty tterm) (reducer (term tterm))))
(right (right (lty tterm) (reducer (term tterm))))
(case-on (let ((on (on tterm))
(ltm (ltm tterm))
(rtm (rtm tterm)))
(cond ((typep on 'left) (substitute-zero on ltm))
((typep on 'right) (substitute-zero on rtm))
(t (case-on (reducer on)
(reducer ltm)
(reducer rtm))))))
(pair (pair (reducer (ltm tterm))
(reducer (rtm tterm))))
(fst (let ((term (term tterm)))
(if (typep (reducer term) 'pair)
(reducer (ltm term))
(fst (reducer term)))))
(snd (let ((term (term tterm)))
(if (typep (reducer term) 'pair)
(reducer (rtm term))
(snd (reducer term)))))
(lamb (lamb (tdom tterm) (reducer (term tterm))))
(app
(let ((fun (fun tterm))
(term (car (term tterm))))
(cond ((typep fun 'lamb)
(substitute-zero (reducer term) (reducer (term fun))))
((and (typep fun 'case-on)
(typep (ltm fun) 'lamb)
(typep (rtm fun) 'lamb))
(let ((irec (index-excess (reducer term))))
(flet ((zero-index (term)
(substitute-zero irec (reducer (term term)))))
(reducer (case-on (reducer (on fun))
(zero-index (ltm fun))
(zero-index (rtm fun)))))))
((and (typep fun 'case-on)
(typep (ltm fun) 'lamb)
(typep (rtm fun) 'case-on))
(reducer (case-on (reducer (on fun))
(substitute-zero (index-excess (reducer term))
(reducer (term (ltm fun))))
(reducer (app (rtm fun)
(list (index-excess term)))))))
((and (typep fun 'case-on)
(typep (ltm fun) 'lamb)
(typep (rtm fun) 'case-on))
(reducer (case-on (reducer (on fun))
(reducer (app (ltm fun)
(list (index-excess term))))
(substitute-zero (index-excess (reducer term))
(reducer (term (rtm fun)))))))
((typep fun 'err)
(err (mcadr (ttype fun))))
(t (app (reducer fun) (list (reducer term)))))))
((or lamb-eq
lamb-lt)
(let ((ltm (ltm tterm))
(rtm (rtm tterm)))
(if (and (typep ltm 'bit-choice)
(typep rtm 'bit-choice))
(if (funcall (dispatch-arith tterm)
(bitv ltm)
(bitv rtm))
(left so1 (unit))
(right so1 (unit)))
(funcall (dispatch tterm)
(reducer ltm)
(reducer rtm)))))
((or plus
times
minus
divide
modulo)
(let ((ltm (ltm tterm))
(rtm (rtm tterm)))
(if (and (typep ltm 'bit-choice)
(typep rtm 'bit-choice))
(bit-choice
(funcall (dispatch-arith tterm)
(bitv ltm)
(bitv rtm)))
(funcall (dispatch tterm)
(reducer ltm)
(reducer rtm)))))
((or unit
index
err
bit-choice)
tterm)))

(defun substitute-zero (replaced-term replacing-term)
"Substitutes the zero'th index, and properly marks it"
(delist (index-lack 0 (sub 0 replaced-term replacing-term))))
1 change: 1 addition & 0 deletions src/lambda/package.lisp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,7 @@
(fun-type pax:class)
(fun-type pax:function)
(errorp pax:function)
(reducer pax:function)

(mcar (pax:method () (fun-type)))
(mcadr (pax:method () (fun-type)))
Expand Down
Loading

0 comments on commit 06b05b7

Please sign in to comment.