A more idiomatic approach to code lowering. λ symbolizes a process for defining the ways to do something. ☶ symbolizes a process for selecting the natural way to do something. λ answers "why is this correct?" ☶ answers "why is this desirable?"
λ☶ is a programming language written in the passive voice.
eval-soft and eval-hard are the exposed entry points into your program.
A λ☶ program is then defined as capabilities gifted to anyone with access to your entry points.
Each program defines a policy and implementation of capabilities.
Any attempt to subvert these policies should result in an error instead of actual evaluation.
Syntactically, capabilities are exposed to the user as globally bound variables.
User-land programs can then be thought of as simple lambda-calculus expressions.
Below is an example of a user-land program containing one policy bound to the variable print.
User programs can be any unicode text. Anything. Really. "Free Grammar!"
λ-calculus
print "hello world"
The "string" syntax from the above program needs to be rewritten into a lambda-calculus expression. Grammatical Rewriting is accomplished in the policy definition as follows.
λ☶
::pre := λ["] (literal s) ["]. s
::pre := λc (::pre cs). c cs
literal := λc (literal cs). c cs
Each bound variable gets its own line in the policy definition.
λ☶
print := λmsg. org 0x100 \n (splat msg) mov ah, 0x4c \n int 0x21 \n
splat := λc cs. mov dl, c \n mov ah, 2 \n int 0x21 \n (splat cs)
The x86 assembler output here needs to be compiled and run. This is accomplished in the policy definition as follows.
λ☶
::post := λeval-result. ... side effects go here ...
soft reductions will not diverge and are strongly normalizing.
if a term may diverge then an error may occur.
blame is defined by the rewrite rules.
hard reductions are evaluations until normal form and may diverge.
bash
lambda_mountain print.lm < print.txt
The magic really starts to happen when we connect the above term definitions with intelligent equivalences. Equivalences are defined by rewrite rules that look like this:
Stylistic considerations are important when proof trees start to look like this:
