-
Notifications
You must be signed in to change notification settings - Fork 4
/
README
76 lines (51 loc) · 2.15 KB
/
README
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
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.