### lambda.sed
### a reducer for the lambda calculus


### Note: (March 15, 1999)
### The paren-renaming shortcut causes this to break in
### certain pathological cases (like Y :).
### (\x.x x), for example, duplicates the `unique' names.
### It seemed like a good idea at the time ... :)


### There are three possible expressions
###   a variable:       x
###   a function:       (\x.E)
###   an application:   (E1 E2)

### In the function (\x.E), we see four units of structure:
###   enclosing parentheses
###   the symbol, lambda, \
###   the single formal parameter, x
###   and the funtion body, E

### In a function application, we replace all occurances of the
### formal parameter in the body with the argument.
### This is called beta-reduction.
### For example, ((\x.(x y)) z) becomes (z y).
### This can cause variable capture if there are functions
### that use the same variable name.
### The reduction of (((\x.(\y.(y x))) u) t) proceeds as follows:
###   ((\y.((\x.(y x)) u)) t)
###   ((\x.(t x)) u)
###   (t u)
### not:
###   ((\y.((\x.(y x)) u)) x)
###   ((\x.(x x)) u)
###   (u u)
###
### One way to avoid this problem is by check for, and changing
### the names of conflicting variables.  Changing the names
### of variables is called alpha-conversion.
### We don't do that.  We avoid this problem by insisting that
### all variable names are unique integers.

### Nested parentheses cause problems in sed.
### Jeffrey Friedl makes the observation:
###   ``In fact, the problem is that you simply can't match
###   arbitrarily nested constructs with regular expressions.
###   It just can't be done.'' [Friedl 97]
###
### To combat this, we adopt an alternative representation --
### we will uniquely name our parentheses (unique, also, from
### those we use for variables).

### Another thing to be careful of, is the order of evaluation.
### Strict evaluation (evaluating the argument before it being
### adopted as a function argument) can reduce the number of
### reduction steps, but can result in non-termination.
### The alternative is the call-by-name approach, where the
### argument is simply copied verbatim into the body.
### This is guaranteed to terminate if termination is possible.
### This is what we do.  We're in no rush.

### One shorthand: in the application ((\x.E) y), when we want to
### show its evaluation for an arbitrary E, we use the notation,
### E[y/x].  Ie, E with all xs replaced with ys.

### This leaves us with the following modified expressions:
###   a variable:       i
###   a function:       (j=E=j)
###   an application:   (:k:E1-k-E2:k:)

### We need some way to reduce sub-problems in the reduction process.
### We keep the currently reducing expression at the beginning of the
### line.  If we have to push a context, we stick it at the end of
### the line.  We introduce two special symbols for this process, X and |.
### Given the expression, (((\x.x) (\y.a)) b), we pull out the first
### element of the outermost application, ((\x.x) (\y.a)) and remember
### the rest as (X b), where X will be replaced with out reduced expression.
### This gives us a stack that looks like:
###     ((\x.x) (\y.a))|(X b)
### The top problem is waiting excitedly for beta-reduction, so we relieve it.
###     (\y.a)|(X b)
### Simplified, we replace this expression back into the waiting application.
###     ((\y.a) b)
### Which reduces to a.

### Numbers are represented with church numbers:
### 0 = (\f.(\x.x))          = (0=(1=1=1)=0)
### 1 = (\f.(\x.(f x)))      = (0=(1=(:2:0-2-1:2:)=1)=0)
### 2 = (\f.(\x.(f (f x))))  = (0=(1=(:2:0-2-(:3:0-3-1:3:):2:)=1)=0)
### ...
### n = (\f.(\x.(f^n x)))

### Test cases
### zero
###     (\f.(\x.x))
###     (1=(2=2=2)=1)
### suc
###     (\n.(\f.(\x.((n f) (f x)))))
###     (1=(2=(3=(:4:(:5:1-5-2:5:)-4-(:6:2-6-3:6:):4:)=3)=2)=1)
### true
###     (\x.(\y.x))
###     (1=(2=1=2)=1)
### false
###     (\x.(\y.y))
###     (1=(2=2=2)=1)
### if
###     (\p.(\x.(\y.((p x) y))))
###     (1=(2=(3=(:4:(:5:1-5-2:5:)-4-3:4:)=3)=2)=1)
### iszero
###     (\n.((n (\x.false)) true))
###     (1=(:2:(:3:1-3-(4=false=4):3:)-2-true:2:)=1)
###     (1=(:2:(:3:1-3-(4=(5=(6=6=6)=5)=4):3:)-2-(7=(8=7=8)=7):2:)=1)
### (iszero zero)
###     ((\n.((n (\x.false)) true)) (\f.(\x.x)))
###     ((\n.((n (\x.(\a.(\b.b)))) (\c.(\d.c)))) (\f.(\x.x)))
###     (((\f.(\x.x)) (\x.(\a.(\b.b)))) (\c.(\d.c)))
###     ((\x.x) (\c.(\d.c)))
###     (\c.(\d.c)) == true
###     (:0:(1=(:2:(:3:1-3-(4=(5=(6=6=6)=5)=4):3:)-2-(7=(8=7=8)=7):2:)=1)-0-(9=(10=10=10)=9):0:)
###     (:2:(:3:(9=(10=10=10)=9)-3-(4=(5=(6=6=6)=5)=4):3:)-2-(7=(8=7=8)=7):2:)
###     (:2:(:3:(9=(10=10=10)=9)-3-(4=(5=(6=6=6)=5)=4):3:)-2-(7=(8=7=8)=7):2:)
###     (:3:(9=(10=10=10)=9)-3-(4=(5=(6=6=6)=5)=4):3:)|(:2:X-2-(7=(8=7=8)=7):2:)
###     (10=10=10)|(:2:X-2-(7=(8=7=8)=7):2:)
###     (:2:(10=10=10)-2-(7=(8=7=8)=7):2:)
###     (7=(8=7=8)=7) == true
### (suc zero)
###     ((\n.(\f.(\x.((n f) (f x))))) (\f.(\x.x)))
###     (\f.(\x.(((\f.(\x.x)) f) (f x))))
###     (\x.(((\f.(\x.x)) f) (f x)))|(\f.X)
###     (((\f.(\x.x)) f) (f x))|(\x.X)|(\f.X)
###     ((\f.(\x.x)) f)|(X (f x))|(\x.X)|(\f.X)
###     (\x.x)|(X (f x))|(\x.X)|(\f.X)
###     ((\x.x) (f x))|(\x.X)|(\f.X)
###     (f x)|(\x.X)|(\f.X)
###     (\x.(f x))|(\f.X)
###     (\f.(\x.(f x))) == 1
###     (:1:(2=(3=(4=(:5:(:6:2-6-3:6:)-5-(:7:3-7-4:7:):5:)=4)=3)=2)-1-(8=(9=9=9)=8):1:)
###     (3=(4=(:5:(:6:(8=(9=9=9)=8)-6-3:6:)-5-(:7:3-7-4:7:):5:)=4)=3)
###     (4=(:5:(:6:(8=(9=9=9)=8)-6-3:6:)-5-(:7:3-7-4:7:):5:)=4)|(3=X=3)
###     (:5:(:6:(8=(9=9=9)=8)-6-3:6:)-5-(:7:3-7-4:7:):5:)|(4=X=4)|(3=X=3)
###     (:6:(8=(9=9=9)=8)-6-3:6:)|(:5:X-5-(:7:3-7-4:7:):5:)|(4=X=4)|(3=X=3)
###     (9=9=9)|(:5:X-5-(:7:3-7-4:7:):5:)|(4=X=4)|(3=X=3)
###     (:5:(9=9=9)-5-(:7:3-7-4:7:):5:)|(4=X=4)|(3=X=3)
###     (:7:3-7-4:7:)|(4=X=4)|(3=X=3)
###     (4=(:7:3-7-4:7:)=4)|(3=X=3)
###     (3=(4=(:7:3-7-4:7:)=4)=3) = 1

### To make it easy to reason about whether we're going up or down the
### recursion stack, we introduce two varieties of our already-complex
### paren nameing scheme.
### We form two groups, complex and simple.
### When we get the initial form to reduce, we mark it as complex,
### and as we reduce, it becomes progressively simpler and is marked as such.
### Simple syntax will remain as we have specified above.
### Complex syntax will simply double the =s, :s and -s.
### An application's arguments are indicated separately,
### i.e., simple: (:1:a-1-b:1:), simple op: (:1:-a--b::1::), etc.
###
### Taking zero, as above, as an example, we get as input:
###     (1=(2=2=2)=1)
### Our first step is to mark it as complex:
###     (1==(2==2==2)==1)
### and reduce:
###     (2==2==2)|(1==X==1)
### At a recursion-terminating statement, we mark it as simplified,
###     (2=2=2)|(1==X==1)
### pop,
###     (1==(2=2=2)==1)
### and simple expressions containing simplified elements are declared simplified
###     (1=(2=2=2)=1)

### References
###
### Friedl, Jeffrey E.F.
### Mastering Regular Expressions
### O'Reilly and Associates, Inc., March 1997
###
### Paulson, L.C.
### ML for the Working Programmer, 2nd edition
### Cambridge University Press, 1996


### make it complex
s/\([-:=]\)/\1\1/g

:loop

/.*/p

### variable
# variable with stack => pop
s/^\([[:digit:]]\+\)|\([^|]\+\)X\(.*\)/\2\1\3/
# variable without stack => exit
/^[[:digit:]]\+$/b end

### lambda
# short-cut when body of lambda is variable
s/^(\([[:digit:]]\+\)==\([[:digit:]]\+\)==\1)\(.*\)/(\1=\2=\1)\3/
# complex lambda => recurse
s/^(\([[:digit:]]\+\)==\([^|]\+\)==\1)\(.*\)/\2|(\1=X=\1)\3/
# simple lambda with stack => pop
s/^(\([[:digit:]]\+\)=\([^=][^|]*\)=\1)|\([^|X]\+\)X\(.*\)/\3(\1=\2=\1)\4/
# simple lambda without stack => exit
/^(\([[:digit:]]\+\)=\([^|]\+\)=\1)$/b end
t loop

### application
### (var x) == simplify x, then simplified
### (lambda x) == simplify lambda, substitute x for lambda var and mark as complex
### (app x) == simplify app, simplify x, then simplified
### generally, simplify operator, substitute if possible, else simplify operand
## if operator is lambda, simplified or not => beta reduce, ([x/y] E)
# here we simplify on the way down
s_^(::\([[:digit:]]\+\)::(\([[:digit:]]\+\)==\([^|]\+\)==\2)--\1--\([^|]\+\)::\1::)\(.*\)_[\4/\2] \3\5_
# and on the way up
s_^(:\([[:digit:]]\+\):(\([[:digit:]]\+\)=\([^|]\+\)=\2)-\1-\([^|]\+\):\1:)\(.*\)_[\4/\2] \3\5_
# substitute
:subst
s,^\[\([^/]\+\)/\([[:digit:]]\+\)\] \2\(.*\),\[\1/\2] \1\3,
s,^\[\([^/]\+\)/\([[:digit:]]\+\)\] \([^|]*[^[:digit:]]\)\2\([^[:digit:]].*\),\[\1/\2] \3\1\4,
t subst
s,^[^ ]\+ ,,
# no longer know as much about it being simplified, so make it all complex again
#s/\([-:=]{1}\)/\1\1/g
t loop
# if operator is complex, reduce operator
s/^(::\([[:digit:]]\+\)::\([^|]\+\)--\(\1-\+[^|]\+:\+\1:\+)\)\(.*\)/\2|(:\1:X-\3\4/
## if operator is simplified, but not a lambda, we simplify the argument
# (can assume operator is not a lambda, here)
s/^(:\([[:digit:]]\+\):\([^|]\+\)-\1--\([^|]\+\)::\1::)\(.*\)/\3|(:\1:\2-\1-X:\1:)\4/
t loop
# both simplified, but operator not lambda
# (If we got this far, the operator cannot both be simplified and be a lambda,
# so if it's simplified, we just return it)
# without stack
/^(:\([[:digit:]]\+\):\([^|]\+\)-\1-\([^|]\+\):\1:)$/b end
# with stack
s/^(:\([[:digit:]]\+\):\([^|]\+\)-\1-\([^|]\+\):\1:)|\([^X]*\)X\(.*\)/\4(:\1:\2-\1-\3:\1:)\5/

b loop

:end