Unlambda abstraction elimination (Sed)
From LiteratePrograms
- Other implementations: C++ | Sed
This program does Unlambda abstraction elimination. Lambda syntax is the same as on the Unlambda home page, except that the dollar signs are omitted. That is, instead of e.g. ^x`$xi you just write ^x`xi (which results in ``si`ki). Currently, whitespace is not allowed in the expression.
Contents |
Theory
Practice
We code the naive algorithm from Madore:
Finally, abstraction elimination is described mechanically as follows: consider the expression F and we want to eliminate the lambda from ^xF. Scan the F expression from left to right: for every ` (backquote) encountered, write ``s (by virtue of the third case above); for every $x encountered, write i (by virtue of the second case); and for any builtin or any variable other than $x, write `k followed by the thing in question.
As whitespace isn't allowed in the expression, we use space as the cursor, followed by a single character containing the variable abstracted by the λ.
- each ` is converted to ``s
<<handle applications>>= s/ \(.\)`/``s \1/;tloop
- each instance of the variable is converted to i.
<<handle substitutions>>= s/ \(.\)\1/i \1/;tloop
- and builtins or other variables are prefixed by `k
<<handle constants>>= s/ \(.\)\(\..\)/`k\2 \1/;tloop s/ \(.\)\(\?.\)/`k\2 \1/;tloop s/ \(.\)\(.\)/`k\2 \1/;tloop
we will also provide the loop entry point (:loop), and arrange to eliminate the cursor once it reaches the end of the scan ($)
<<abstraction elimination>>= :loop handle applications handle substitutions handle v optimization handle constants s/ .$//
multiple λs
If several lambdas need to be eliminated from one expression, the trick is to start with the innermost ones, and to eliminate the outermost lambdas last. As an example, ^x^y`$y$x becomes first ^x``si`k$x (upon eliminating the innermorst lambda) and then ``s``s`ks`ki``s`kki (upon eliminating the outermost).
Proceeding from innermost to outermost λs means that we will always choose the last ^ in the expression to eliminate; looping until we have no more ^s left.
<<uae.sed>>= belim abstraction elimination :elim s/\(.*\)\^\(.\)/\1 \2/;tloop
minor optimization
Note also that the V builtin can always be abstracted to itself. (That is, `kv is functionally identical to v.)
<<handle v optimization>>= s/ \(.\)v/v \1/;tloop
Exercise: implement the other rewriting optimizations mentioned by Madore or found in the C++ implementation
Wrapping up
Finally, we try a few small test cases:
^xx i ^xa `ka ^x`xi ``si`ki ^x^y`yx ``s``s`ks`ki``s`kki
| Download code |