Skip to content

Commit 2031a4d

Browse files
Sn0rtSn0rt
committed
opt: replace bool and number with lambda expr
Signed-off-by: Sn0rt <[email protected]>
1 parent 09b3652 commit 2031a4d

File tree

8 files changed

+1236
-514
lines changed

8 files changed

+1236
-514
lines changed

‎.gitignore‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,2 +1,4 @@
11
/target
2-
.idea
2+
.idea
3+
docs/states/*
4+
docs/*.out

‎README.md‎

Lines changed: 18 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -14,12 +14,10 @@ The interpreter supports the following instructions and operations:
1414
2. **Church Numerals**
1515
- Encoding: Automatically handled by the interpreter
1616
- Decoding: Automatically handled by the interpreter
17-
- Addition: `add`
18-
- Subtraction: `subtract`
19-
- Multiplication: `multiply`
2017
- Predecessor: `pred`
2118
- Successor: `succ`
2219
- Is Zero: `is_zero`
20+
- Multiplication: `multiply` or `*`
2321

2422
3. **Church Booleans**
2523
- True: `true` (encoded as `λx. λy. x`)
@@ -29,12 +27,12 @@ The interpreter supports the following instructions and operations:
2927
- Not: `not`
3028

3129
4. **Control Flow**
32-
- If-Then-Else: `ifelse`
30+
- If-Then-Else: `ifthenelse`
3331

3432
5. **Pairs**
3533
- Create Pair: `pair`
36-
- First Element: `fst`
37-
- Second Element: `snd`
34+
- First Element: `first`
35+
- Second Element: `second`
3836

3937
6. **Recursion**
4038
- Y Combinator: `Y`
@@ -43,9 +41,11 @@ The interpreter supports the following instructions and operations:
4341

4442
Here are some examples of how to use the interpreter:
4543

46-
1. Church Numeral Addition:
44+
1. Church Numeral Operations:
4745
```
48-
(add (church_encode 2) (church_encode 3))
46+
(multiply 2 3)
47+
(is_zero 0)
48+
(pred (succ 5))
4949
```
5050

5151
2. Boolean Operations:
@@ -57,18 +57,21 @@ Here are some examples of how to use the interpreter:
5757

5858
3. Conditional Statement:
5959
```
60-
(ifelse (is_zero 0) 42 58)
60+
(ifthenelse (is_zero 0) 1 2)
6161
```
6262

63-
4. Factorial using Y Combinator:
63+
4. Pair Operations:
6464
```
65-
(Y (λf. λn. (ifelse (is_zero n) 1 (multiply n (f (pred n))))))
65+
(pair 1 2)
66+
(first (pair 1 2))
67+
(second (pair 1 2))
68+
```
69+
70+
5. Factorial using Y Combinator:
71+
```
72+
(Y (λf. λn. (ifthenelse (is_zero n) 1 (multiply n (f (pred n))))))
6673
```
6774

6875
## Running Tests
6976

7077
To run the tests and see examples of the interpreter in action, use the following command:
71-
72-
```rust
73-
$ cargo test
74-
```

‎docs/LambdaOP.cfg‎

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
(**********************************************)
2+
(* Initial predicate and next-state relation. *)
3+
(* Alternatively, you can comment out these *)
4+
(* and use SPECIFICATION. *)
5+
(**********************************************)
6+
7+
(**********************************************)
8+
(* Specify the values of declared constants. *)
9+
(**********************************************)
10+
\* CONSTANT MyConstant = {0, 1}
11+
12+
(**********************************************)
13+
(* Formulas true in every reachable state. *)
14+
(**********************************************)
15+
\* INVARIANT MyInvariant
16+
17+
(**********************************************)
18+
(* Disable checking deadlock. *)
19+
(**********************************************)
20+
\* CHECK_DEADLOCK FALSE
21+
22+
SPECIFICATION Spec
23+
24+
CONSTANT
25+
MaxDepth = 20
26+
27+
INVARIANT TypeOK
28+
INVARIANT DepthInvariant
29+
30+
CHECK_DEADLOCK FALSE

‎docs/LambdaOP.tla‎

Lines changed: 220 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,220 @@
1+
---- MODULE LambdaOP ----
2+
EXTENDS Naturals, Sequences, TLC
3+
4+
CONSTANT MaxDepth
5+
6+
VARIABLE evalStack, depth, currentOp
7+
8+
ToNumber(churchNumeral) ==
9+
CASE churchNumeral.type = "ChurchNumeral" -> churchNumeral.value
10+
[] OTHER -> 0
11+
12+
Max(a, b) == IF a > b THEN a ELSE b
13+
14+
(* Basic Lambda Calculus *)
15+
Variable(name) == [type |-> "Variable", value |-> name, left |-> [type |-> "", value |-> ""], right |-> [type |-> "", value |-> ""]]
16+
17+
Abstraction(param, body) == [type |-> "Abstraction", value |-> "lambda", left |-> Variable(param), right |-> body]
18+
19+
Application(func, arg) == [type |-> "Application", value |-> "apply", left |-> func, right |-> arg]
20+
21+
(* Church Numerals *)
22+
ChurchNumeral(n) ==
23+
[type |-> "ChurchNumeral",
24+
value |-> n,
25+
left |-> [type |-> "", value |-> ""],
26+
right |-> [type |-> "", value |-> ""]]
27+
28+
Succ ==
29+
[type |-> "Builtin", value |-> "succ",
30+
left |-> [type |-> "", value |-> ""],
31+
right |-> [type |-> "", value |-> ""]]
32+
33+
Pred ==
34+
[type |-> "Builtin", value |-> "pred",
35+
left |-> [type |-> "", value |-> ""],
36+
right |-> [type |-> "", value |-> ""]]
37+
38+
IsZero ==
39+
[type |-> "Builtin", value |-> "is_zero",
40+
left |-> [type |-> "", value |-> ""],
41+
right |-> [type |-> "", value |-> ""]]
42+
43+
Multiply ==
44+
[type |-> "Builtin", value |-> "multiply",
45+
left |-> [type |-> "", value |-> ""],
46+
right |-> [type |-> "", value |-> ""]]
47+
48+
(* Church Booleans *)
49+
ChurchTrue ==
50+
Abstraction("x", Abstraction("y", Variable("x")))
51+
52+
ChurchFalse ==
53+
Abstraction("x", Abstraction("y", Variable("y")))
54+
55+
And ==
56+
[type |-> "Builtin", value |-> "and",
57+
left |-> [type |-> "", value |-> ""],
58+
right |-> [type |-> "", value |-> ""]]
59+
60+
Or ==
61+
[type |-> "Builtin", value |-> "or",
62+
left |-> [type |-> "", value |-> ""],
63+
right |-> [type |-> "", value |-> ""]]
64+
65+
Not ==
66+
[type |-> "Builtin", value |-> "not",
67+
left |-> [type |-> "", value |-> ""],
68+
right |-> [type |-> "", value |-> ""]]
69+
70+
(* Control Flow *)
71+
IfThenElse ==
72+
[type |-> "Builtin", value |-> "ifthenelse",
73+
left |-> [type |-> "", value |-> ""],
74+
right |-> [type |-> "", value |-> ""]]
75+
76+
(* Pairs *)
77+
Pair ==
78+
[type |-> "Builtin", value |-> "pair",
79+
left |-> [type |-> "", value |-> ""],
80+
right |-> [type |-> "", value |-> ""]]
81+
82+
First ==
83+
[type |-> "Builtin", value |-> "first",
84+
left |-> [type |-> "", value |-> ""],
85+
right |-> [type |-> "", value |-> ""]]
86+
87+
Second ==
88+
[type |-> "Builtin", value |-> "second",
89+
left |-> [type |-> "", value |-> ""],
90+
right |-> [type |-> "", value |-> ""]]
91+
92+
(* Recursion *)
93+
YCombinator ==
94+
[type |-> "Builtin", value |-> "Y",
95+
left |-> [type |-> "", value |-> ""],
96+
right |-> [type |-> "", value |-> ""]]
97+
98+
EvalSucc ==
99+
/\ Len(evalStack) > 0
100+
/\ depth < MaxDepth
101+
/\ LET n == Head(evalStack)
102+
IN /\ evalStack' = Tail(evalStack) \o <<ChurchNumeral(ToNumber(n) + 1)>>
103+
/\ depth' = depth + 1
104+
105+
EvalPred ==
106+
/\ Len(evalStack) > 0
107+
/\ depth < MaxDepth
108+
/\ LET n == Head(evalStack)
109+
IN /\ evalStack' = Tail(evalStack) \o <<ChurchNumeral(Max(0, ToNumber(n) - 1))>>
110+
/\ depth' = depth + 1
111+
112+
EvalIsZero ==
113+
/\ Len(evalStack) > 0
114+
/\ LET n == Head(evalStack)
115+
IN /\ evalStack' = Tail(evalStack) \o <<IF ToNumber(n) = 0 THEN ChurchTrue ELSE ChurchFalse>>
116+
/\ depth' = depth + 1
117+
118+
EvalMultiply ==
119+
/\ Len(evalStack) > 1
120+
/\ depth < MaxDepth
121+
/\ LET n == Head(evalStack)
122+
m == Head(Tail(evalStack))
123+
IN /\ evalStack' = Tail(Tail(evalStack)) \o <<ChurchNumeral(ToNumber(n) * ToNumber(m))>>
124+
/\ depth' = depth + 1
125+
126+
EvalAnd ==
127+
/\ Len(evalStack) > 1
128+
/\ LET b1 == Head(evalStack)
129+
b2 == Head(Tail(evalStack))
130+
IN /\ evalStack' = Tail(Tail(evalStack)) \o <<IF b1 = ChurchTrue /\ b2 = ChurchTrue THEN ChurchTrue ELSE ChurchFalse>>
131+
/\ depth' = depth + 1
132+
133+
EvalOr ==
134+
/\ Len(evalStack) > 1
135+
/\ LET b1 == Head(evalStack)
136+
b2 == Head(Tail(evalStack))
137+
IN /\ evalStack' = Tail(Tail(evalStack)) \o <<IF b1 = ChurchTrue \/ b2 = ChurchTrue THEN ChurchTrue ELSE ChurchFalse>>
138+
/\ depth' = depth + 1
139+
140+
EvalNot ==
141+
/\ Len(evalStack) > 0
142+
/\ LET b == Head(evalStack)
143+
IN /\ evalStack' = Tail(evalStack) \o <<IF b = ChurchTrue THEN ChurchFalse ELSE ChurchTrue>>
144+
/\ depth' = depth + 1
145+
146+
EvalIfThenElse ==
147+
/\ Len(evalStack) > 2
148+
/\ LET condition == Head(evalStack)
149+
thenBranch == Head(Tail(evalStack))
150+
elseBranch == Head(Tail(Tail(evalStack)))
151+
IN /\ evalStack' = Tail(Tail(Tail(evalStack))) \o <<IF condition = ChurchTrue THEN thenBranch ELSE elseBranch>>
152+
/\ depth' = depth + 1
153+
154+
EvalPair ==
155+
/\ Len(evalStack) > 1
156+
/\ LET first == Head(evalStack)
157+
second == Head(Tail(evalStack))
158+
IN /\ evalStack' = Tail(Tail(evalStack)) \o <<[type |-> "Pair", left |-> first, right |-> second]>>
159+
/\ depth' = depth + 1
160+
161+
EvalFirst ==
162+
/\ Len(evalStack) > 0
163+
/\ LET pair == Head(evalStack)
164+
IN /\ evalStack' = Tail(evalStack) \o <<pair.left>>
165+
/\ depth' = depth + 1
166+
167+
EvalSecond ==
168+
/\ Len(evalStack) > 0
169+
/\ LET pair == Head(evalStack)
170+
IN /\ evalStack' = Tail(evalStack) \o <<pair.right>>
171+
/\ depth' = depth + 1
172+
173+
EvalYCombinator ==
174+
(* Y combinator implementation *)
175+
UNCHANGED <<evalStack, depth>>
176+
177+
Init ==
178+
/\ evalStack = <<ChurchNumeral(3), ChurchNumeral(2)>>
179+
/\ depth = 0
180+
/\ currentOp = "none"
181+
182+
Next ==
183+
/\ depth < MaxDepth
184+
/\ \/ /\ currentOp = "none"
185+
/\ \/ /\ currentOp' = "succ"
186+
/\ UNCHANGED <<evalStack, depth>>
187+
\/ /\ currentOp' = "pred"
188+
/\ UNCHANGED <<evalStack, depth>>
189+
\/ /\ currentOp' = "multiply"
190+
/\ UNCHANGED <<evalStack, depth>>
191+
\/ /\ UNCHANGED <<currentOp, evalStack, depth>>
192+
\/ /\ currentOp = "succ"
193+
/\ EvalSucc
194+
/\ currentOp' = "none"
195+
\/ /\ currentOp = "pred"
196+
/\ EvalPred
197+
/\ currentOp' = "none"
198+
\/ /\ currentOp = "multiply"
199+
/\ EvalMultiply
200+
/\ currentOp' = "none"
201+
\/ /\ depth >= MaxDepth
202+
/\ UNCHANGED <<evalStack, depth, currentOp>>
203+
204+
Termination == depth >= MaxDepth
205+
206+
Spec == Init /\ [][Next]_<<evalStack, depth, currentOp>> /\ WF_<<evalStack, depth, currentOp>>(Next) /\ SF_<<evalStack, depth, currentOp>>(Termination)
207+
208+
TypeOK ==
209+
/\ evalStack \in Seq([type: {"ChurchNumeral"},
210+
value: Nat,
211+
left: [type: STRING, value: STRING],
212+
right: [type: STRING, value: STRING]])
213+
/\ depth \in 0..MaxDepth
214+
/\ currentOp \in {"none", "succ", "pred", "multiply"}
215+
216+
DepthInvariant == depth <= MaxDepth
217+
218+
THEOREM Spec => [](TypeOK /\ DepthInvariant)
219+
220+
====

‎docs/LambdaVM.cfg‎

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
(**********************************************)
2+
(* Specify the values of declared constants. *)
3+
(**********************************************)
4+
\* CONSTANT MyConstant = {0, 1}
5+
6+
(**********************************************)
7+
(* Formulas true in every reachable state. *)
8+
(**********************************************)
9+
\* INVARIANT MyInvariant
10+
11+
(**********************************************)
12+
(* Disable checking deadlock. *)
13+
(**********************************************)
14+
\* CHECK_DEADLOCK FALSE
15+
16+
SPECIFICATION VMSpec
17+
18+
CONSTANTS
19+
VMMaxDepth = 100
20+
MaxExprDepth = 5
21+
Variables = {"x", "y", "z"}
22+
MaxSubstituteDepth = 20
23+
24+
INVARIANT VMTypeOK
25+
26+
\* Uncomment the following line if you want to disable deadlock checking
27+
\* CHECK_DEADLOCK FALSE

0 commit comments

Comments
 (0)