-
Notifications
You must be signed in to change notification settings - Fork 4
A Small Evaluator for Untyped Lambda Calculus
License
sanjoy/L
Folders and files
Name | Name | Last commit message | Last commit date | |
---|---|---|---|---|
Repository files navigation
L: A Small Untyped Lambda Calculus Reduction Machine L is a simple untyped lambda calculus reduction machine. It reads expressions and then reduces them. The current implementation is essentially driven by a primitive REPL. While I'll write more detailed documentation as I get more time, a quick sample of how to interact with the machine follows: First let us enter some definitions into the REPL: :Zero = L a b . b; :Succ = L n f x. f (n f x); Now that the machine knows what these elements are, we can start combining them: :One = :Succ :Zero; Note that the REPL will respond with `:One = :Succ :Zero'. This is because the actual evaluation has not occurred yet. You can view the raw un-computed value stored in `:One' by simply typing `:One' in the REPL. To actually reduce `:One' you have to use the EVAL operator, which is essentially a pair of square braces. You can i. Display the computed value, by entering: [:One]; ii. Update the value stored in the identifier: :One = [:One]; iii. Store the computed value elsewhere: :AnotherOne = [:One]; Please note that you could have simply done a `:One = [:Succ :Zero]' in the first place. As another example, let us calculate 3!. First, the foundations: L > :Zero = L a b . b; L > :Succ = L n f x. f (n f x); L > :Pred = L n f x . n (L g h . h (g f)) (L u . x) (L u . u); L > :One = :Succ :Zero; L > :Three = :Succ (:Succ (:Succ :Zero)); L > :Mult = L m n f. n (m f); Then the conditionals: L > :IfThenElse = L a b c . a b c; L > :True = L a b . a; L > :False = L a b . b; L > :IsZero = L a . a (L t . :False) :True; The factorial function is the fixed-point solution of this equations: L > :FactorialEqn = L f n . :IfThenElse (:IsZero n) :One (:Mult n (f ... (:Pred n))); The combinator to solve the above fixed-point equation. L > :YCombinator = L f.(L x.f (x x)) (L x.f (x x)); The factorial function: L > :ActualFactorial = :YCombinator :FactorialEqn; Then the solution: L > [:ActualFactorial :Three] to give the final solution. L still has a lot of issues; specifically, things like the lack of proper error handling and poor file management are being worked on.
About
A Small Evaluator for Untyped Lambda Calculus
Resources
License
Stars
Watchers
Forks
Releases
No releases published
Packages 0
No packages published