Unlambda abstraction elimination (Sed)

From LiteratePrograms
Jump to: navigation, search
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.


[edit] Theory

[edit] 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>>=
handle applications
handle substitutions
handle v optimization
handle constants
s/ .$//

[edit] 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.

abstraction elimination
s/\(.*\)\^\(.\)/\1 \2/;tloop

[edit] 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

[edit] Wrapping up

Finally, we try a few small test cases:

Download code