You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
@@ -63,6 +63,7 @@ type Environment = [(String, Expr)]
63
63
```
64
64
65
65
Now we can define a compiler that translates such λ-expressions to combinator terms.
66
+
(You will find the complete code in [Kiselyov.hs](https://github.com/thma/lambda-ski/blob/main/src/Kiselyov.hs)
66
67
67
68
Our journey begins by translating λ-expressions to a datatype `DB` which is quite similar to the λ-calculus terms but uses indices instead of variable names.This is done by the function `deBruijn`:
68
69
@@ -108,81 +109,170 @@ The innermost lambda-abstraction binds the variable `y` which is represented by
108
109
This notation is quite helpful as it allows to systematically adress variables by their respective position in a complex term.
109
110
110
111
But why are we using Peano numbers for the indices? Why not just use integers?
111
-
Well it's definitely possible to [use integers instead of Peano numbers](https://crypto.stanford.edu/~blynn/lambda/cl.html).
112
+
Well it's definitely possible to [use integers as indices](https://crypto.stanford.edu/~blynn/lambda/cl.html).
112
113
But there is a good reason to use Peano numbers in our case:
113
-
In the subsequent compilation steps we want to be able to do pattern matching on the indices. This is not possible with integers but it is possible with Peano numbers, because they are defined as an algebraic data type:
114
+
In the subsequent compilation steps we want to be able to do pattern matching on the indices. This is possible with Peano numbers, because they are defined as an algebraic data type:
114
115
115
116
```haskell
116
117
dataPeano=SuccPeano | Zero
117
118
```
118
119
119
-
Starting with the de Bruijn notation BenLynn's implementation ofKiselyov's algorithm builds up a series of increasingly optimized compilers that translate λ-expressions to combinator terms.
120
+
Starting with the de Bruijn notation BenLynn's implementation ofKiselyov's algorithm builds up a series ofsix increasingly optimized compilers that translate λ-expressions to combinator terms:
120
121
121
-
I'll don't want to go into all the details of the algorithm. [Ben's blog post](https://crypto.stanford.edu/~blynn/lambda/kiselyov.html) is a great resource for this.I'll just give a brief overview of the compilation results of the different compilers.
122
+
- a plain compiler without any optimizations (`compilePlain`)
123
+
- a compiler that implements K-optimization (`compileK`)
124
+
- a compiler that implements K-andEta-optimization (`compileEta`)
125
+
- a compiler that generates code with *BulkCombinators* (`compileBulk`)
126
+
- a compiler that eliminates *BulkCombinators* with linear size(`compileBulkLinear`)
127
+
- a compiler that eliminates *BulkCombinators* with logarithmic size(`compileBulkLog`)
122
128
123
-
## The Plain compiler
124
-
``` haskell
125
-
compilePlain::Environment->CL
126
-
compilePlain env =caselookup"main" env of
127
-
Nothing->error"main function missing"
128
-
Just main ->snd$ plain env (deBruijn main)
129
+
I'll don't want to go into all the details of the algorithms. [Ben's blog post](https://crypto.stanford.edu/~blynn/lambda/kiselyov.html) is a great resource for this.I'll just give a brief overview of the compilation outputs of the different compilers.AndthenI'll focus on performance comparisons between the different approaches.
130
+
I will use [my original compiler](https://github.com/thma/lambda-ski/blob/main/src/LambdaToSKI.hs) based on the classic (recursively optimized) bracket abstraction as a baseline for the performance comparisons.
131
+
132
+
### The simple `main` example
133
+
134
+
```haskell
135
+
main = λx y.* x y
136
+
```
137
+
138
+
| Compiler | Output |
139
+
| --- | --- |
140
+
|`benchmark: bracket abstraction`|`MUL`|
141
+
|`compilePlain`|`R I(B S(B(B MUL)(B K I)))`|
142
+
|`compileK`|`R I(B B(B MUL I)))`|
143
+
|`compileEta`|`MUL`|
144
+
|`compileBulk`|`MUL`|
145
+
|`compileBulkLinear`|`MUL`|
146
+
|`compileBulkLog`|`MUL`|
147
+
148
+
From this simple example it's obvious that `compilePlain` and `compileK` generate a lot of redundant code. All the other compilers generate the same output as the baseline.
149
+
150
+
Please also note that the Kiselyov algorithms may emit code for an additional `R` combinator with the following reduction rule:
151
+
152
+
```haskell
153
+
R f g x = g x f
129
154
```
130
155
131
-
The first compiler is called `plain`. It is a straightforward translation of the de Bruijn notation to combinators. It uses the `CL` data type to represent combinator-terms:
156
+
### The factorial function
132
157
133
158
```haskell
134
-
dataCL=ComCombinator | INTInteger | CL:@CL
159
+
fact = y(λf n.if (is0 n) 1 (* n (f (sub1 n))))
160
+
main = fact 100
135
161
136
-
dataCombinator=I | K | S | B | C | Y | R | B' | C' | S' | T |
137
-
ADD | SUB | MUL | DIV | REM | SUB1 | EQL | GEQ | ZEROP
138
-
deriving (Eq, Show)
162
+
-- in de Bruijn Notation
163
+
("fact", A (Free"y") (L (L (A (A (A (Free"if") (A (Free"is0") (NZero))) (IN1)) (A (A (Free"*") (NZero)) (A (N (SuccZero)) (A (Free"sub1") (NZero))))))))
164
+
("main", A (Free"fact") (IN100))
139
165
```
140
166
141
-
The`plain` function is defined as follows:
167
+
| Compiler | Output |
168
+
| --- | --- |
169
+
|`benchmark: bracket abstraction`|`Y(B' S(C' IF ZEROP 1)(B' S MUL(C' S K SUB1))) 100`|
170
+
|`compilePlain`|`Y(B(S(R 1(B IF(B ZEROP I))))(B(S(B MUL I))(R(B SUB1 I)(B S(B K I))))) 100`|
171
+
|`compileK`|`Y(B(S(C(B IF(B ZEROP I)) 1))(B(S(B MUL I))(R(B SUB1 I)(B B I)))) 100`|
172
+
|`compileEta`|`Y(B(S(C(B IF ZEROP) 1))(B(S MUL)(R SUB1 B))) 100`|
173
+
|`compileBulk`|`Y(B(S(C(B IF ZEROP) 1))(B(S MUL)(C C SUB1 B))) 100`|
174
+
|`compileBulkLinear`|`Y(B(S(C(B IF ZEROP) 1))(B(S MUL)(C C SUB1 B))) 100`|
175
+
|`compileBulkLog`|`Y(B(S(C(B IF ZEROP) 1))(B(S MUL)(C C SUB1 B))) 100`|
176
+
177
+
178
+
What's interesting here is that only `compileEta` produces code of the same size as the baseline. All others produce code that uses at least one more combinator. Again `compilePlain` and `compileK` generate the largest code sizes.
179
+
180
+
### The fibonacci function
181
+
182
+
```haskell
183
+
fib = y(λf n.if (is0 n) 1 (if (eql n 1) 1 (+ (f (sub1 n)) (f (sub n 2)))))
184
+
main = fib 10
185
+
186
+
-- in de Bruijn notation
187
+
("fib", A (Free"y") (L (L (A (A (A (Free"if") (A (Free"is0") (NZero))) (IN1)) (A (A (A (Free"if") (A (A (Free"eql") (NZero)) (IN1))) (IN1)) (A (A (Free"+") (A (N (SuccZero)) (A (Free"sub1") (NZero)))) (A (N (SuccZero)) (A (A (Free"sub") (NZero)) (IN2)))))))))
188
+
("main", A (Free"fib") (IN10))
189
+
```
190
+
191
+
| Compiler | Output |
192
+
| --- | --- |
193
+
|`benchmark: bracket abstraction`|`Y(B' S(C' IF ZEROP 1)(B' S(C' IF(C EQL 1) 1)(S' S(B' S(K ADD)(C' S K SUB1))(C' S K(C SUB 2))))) 10`|
194
+
|`compilePlain`|`Y(B(S(R 1(B IF(B ZEROP I))))(B(S(R 1(B IF(R 1(B EQL I)))))(S(B S(B(B ADD)(R(B SUB1 I)(B S(B K I)))))(R(R 2(B SUB I))(B S(B K I)))))) 10`|
195
+
|`compileK`|`Y(B(S(C(B IF(B ZEROP I)) 1))(B(S(C(B IF(C(B EQL I) 1)) 1))(S(B S(B(B ADD)(R(B SUB1 I)(B B I))))(R(C(B SUB I) 2)(B B I))))) 10`|
196
+
|`compileEta`|`Y(B(S(C(B IF ZEROP) 1))(B(S(C(B IF(C EQL 1)) 1))(S(B S(B(B ADD)(R SUB1 B)))(R(C SUB 2) B)))) 10`|
197
+
|`compileBulk`|`Y(B(S(C(B IF ZEROP) 1))(B(S(C(B IF(C EQL 1)) 1))(S2(B2 ADD(C C SUB1 B))(C C(C SUB 2) B)))) 10`|
198
+
|`compileBulkLinear`|`Y(B(S(C(B IF ZEROP) 1))(B(S(C(B IF(C EQL 1)) 1))(B(B S) B S(B B B ADD(C C SUB1 B))(C C(C SUB 2) B)))) 10`|
199
+
|`compileBulkLog`|`Y(B(S(C(B IF ZEROP) 1))(B(S(C(B IF(C EQL 1)) 1))(S B I(B(B S) B) I(S B I B ADD(C C SUB1 B))(C C(C SUB 2) B)))) 10`|
200
+
201
+
202
+
Here we see that `compileEta` produce code of the same size as the baseline. `compileBulk` generates code with one less combinator.
203
+
204
+
Please also note that `compileBulk` now emits code for additional bulk combinators `S2` and `B2`. I'll come back to the semantics of these later.
|Just t <-lookup s env = convert (#) env (deBruijn t)
171
-
|otherwise= (0, Com (fromString s))
210
+
ack = y(λf n m.if (is0 n) (+ m 1) (if (is0 m) (f (sub1 n) 1) (f (sub1 n) (f n (sub1 m)))))
211
+
main = ack 22
212
+
213
+
-- in de Bruijn notation
214
+
("ack", A (Free"y") (L (L (L (A (A (A (Free"if") (A (Free"is0") (N (SuccZero)))) (A (A (Free"+") (NZero)) (IN1))) (A (A (A (Free"if") (A (Free"is0") (NZero))) (A (A (N (Succ (SuccZero))) (A (Free"sub1") (N (SuccZero)))) (IN1))) (A (A (N (Succ (SuccZero))) (A (Free"sub1") (N (SuccZero)))) (A (A (N (Succ (SuccZero))) (N (SuccZero))) (A (Free"sub1") (NZero))))))))))
215
+
("main", A (A (Free"ack") (IN2)) (IN2))
172
216
```
173
217
218
+
| Compiler | Output |
219
+
| --- | --- |
220
+
|`benchmark: bracket abstraction`|`Y(B' S(B S(C'(B S K)(B IF ZEROP)(C ADD 1)))(S'(B S(S(K S)))(B' S(K(S(B IF ZEROP)))(B' S(K K)(C' S(C' S K SUB1)(K 1))))(S'(B S(S(K(B S K))))(C' S K SUB1)(C' S(S(K(B S K)))(K SUB1))))) 2 2`|
221
+
|`compilePlain`|`Y(B(S(B S(R(R 1(B ADD I))(B S(B(B IF)(B(B ZEROP)(B K I)))))))(S(B S(B(B S)(B(B(S(B IF(B ZEROP I))))(B(B(R 1))(R(B(B SUB1)(B K I))(B S(B(B S)(B(B K)(B K I)))))))))(S(B S(B(B S)(R(B(B SUB1)(B K I))(B S(B(B S)(B(B K)(B K I)))))))(B(R(B SUB1 I))(B(B S)(R(B K I)(B S(B(B S)(B(B K)(B K I)))))))))) 2 2`|
|`compileBulk`|`Y(B(S2(C C(C ADD 1)(B B(B IF ZEROP))))(S3(B2(C(B IF ZEROP))(C C2 1(C C SUB1 B)))(S2(B2 B(C C SUB1 B))(C C2 SUB1(B B))))) 2 2`|
225
+
|`compileBulkLinear`|`Y(B(B(B S) B S(C C(C ADD 1)(B B(B IF ZEROP))))(B(B S) B(B(B S) B S)(B B B(C(B IF ZEROP))(C(B(B C) B C) 1(C C SUB1 B)))(B(B S) B S(B B B B(C C SUB1 B))(C(B(B C) B C) SUB1(B B))))) 2 2`|
226
+
|`compileBulkLog`|`Y(B(S B I(B(B S) B) I(C C(C ADD 1)(B B(B IF ZEROP))))(B(B(B(B S) B))(S B I)(B(B S) B) I(S B I B(C(B IF ZEROP))(C(S B I(B(B C) B) I) 1(C C SUB1 B)))(S B I(B(B S) B) I(S B I B B(C C SUB1 B))(C(S B I(B(B C) B) I) SUB1(B B))))) 2 2`|
227
+
228
+
As mentioned in my last post the output size of braxcket abstraction grows quadratic with the number of variables.
229
+
In this case with three variables the output size for the bracket abstraction is already significantly larger than for
230
+
the previous example with two variables.
231
+
232
+
Now the Kiselyov algorithms really start to shine. `compileEta` produces code is significantly smaller as the baseline. And `compileBulk` output is even smaller.
233
+
234
+
235
+
### The tak function
236
+
174
237
```haskell
175
-
The main expression compiled to SICKBY combinator expressions by recursice bracket abstraction:
176
-
MUL
238
+
tak = y(λf x y z. (if (geq y x) z (f (f (sub1 x) y z) (f (sub1 y) z x) (f (sub1 z) x y ))))
239
+
main = tak 742
177
240
178
-
applying plain Kiselyov compilation:
179
-
RI(BS(B(BMUL)(BKI)))
241
+
-- in de Bruijn notation
242
+
("tak",A (Free"y") (L (L (L (L (A (A (A (Free"if") (A (A (Free"geq") (N (SuccZero))) (N (Succ (SuccZero))))) (NZero)) (A (A (A (N (Succ (Succ (SuccZero)))) (A (A (A (N (Succ (Succ (SuccZero)))) (A (Free"sub1") (N (Succ (SuccZero))))) (N (SuccZero))) (NZero))) (A (A (A (N (Succ (Succ (SuccZero)))) (A (Free"sub1") (N (SuccZero)))) (NZero)) (N (Succ (SuccZero))))) (A (A (A (N (Succ (Succ (SuccZero)))) (A (Free"sub1") (NZero))) (N (Succ (SuccZero)))) (N (SuccZero))))))))))
243
+
("main",A (A (A (Free"tak") (IN7)) (IN4)) (IN2))
180
244
```
181
245
182
-
## to be continued...
246
+
| Compiler | Output |
247
+
| --- | --- |
248
+
|`benchmark: bracket abstraction`|`Y(B' S(B'(S(K S))(S(K S))(B' S(K IF)(B' S GEQ K)))(S'(B S(S(K(B S(S(K S))))))(S'(B S(S(K(B S(S(K S))))))(S'(B'(S(K(B'(S(K S)) K S))) K S) K(C' S K SUB1))(C'(B'(S(K(B S K))) S(S(K S)))(C' S K SUB1)(B K K)))(C'(B S(S(K(B'(S(K S)) K S))))(C'(B'(S(K S)) K S)(C' S K SUB1) K)(K K)))) 7 4 2`|
249
+
|`compilePlain`|`Y(B(S(B S(B(B S)(B(R I)(B(B S)(B(B(B IF))(B(S(B S(B(B GEQ)(B K I))))(B(B K)(B K I)))))))))(S(B S(B(B S)(B(B(B S))(S(B S(B(B S)(B(B(B S))(S(B S(B(B S)(B(B(B S))(B(B(B K))(B(B K)(B K I))))))(B(B(R I))(B(B(B S))(B(R(B K I))(B(B S)(B(B(B S))(R(B(B(B SUB1))(B(B K)(B K I)))(B S(B(B S)(B(B(B S))(B(B(B K))(B(B K)(B K I))))))))))))))))(R(B(B K)(B K I))(B S(B(B S)(B(B(B S))(B(B(R I))(B(B(B S))(B(R(B(B SUB1)(B K I)))(B(B S)(B(B(B S))(B(B(B K))(B(B K)(B K I))))))))))))))))(B(R(B K I))(B(B S)(B(B(B S))(R(B(B K)(B K I))(B S(B(B S)(B(B(B S))(B(B(R(B SUB1 I)))(B(B(B S))(B(B(B K))(B(B K)(B K I)))))))))))))) 7 4 2`|
|`compileBulk`|`Y(B(S3(B2 IF(C GEQ)))(S4(S4(S B3(C C SUB1 B))(B C2(C C SUB1 B)))(B2 C(B C(C C SUB1 B))))) 7 4 2`|
253
+
|`compileBulkLinear`|`Y(B(B(B S) B(B(B S) B S)(B B B IF(C GEQ)))(B(B S) B(B(B S) B(B(B S) B S))(B(B S) B(B(B S) B(B(B S) B S))(S(B B(B B B))(C C SUB1 B))(B(B(B C) B C)(C C SUB1 B)))(B B B C(B C(C C SUB1 B))))) 7 4 2`|
254
+
|`compileBulkLog`|`Y(B(B(B(B(B S) B))(S B I)(B(B S) B) I(S B I B IF(C GEQ)))(S B I(S B I(B(B S) B)) I(S B I(S B I(B(B S) B)) I(S(B(B B)(S B I) B)(C C SUB1 B))(B(S B I(B(B C) B) I)(C C SUB1 B)))(S B I B C(B C(C C SUB1 B))))) 7 4 2`|
255
+
256
+
In this example with four variables the trend continues. `compileEta` produces code is significantly smaller as the baseline. And `compileBulk` output now is only about 1/3 of the baseline.
257
+
183
258
184
259
## performance comparison
185
260
261
+
So far we have seen that for functions with more than two variables the Kiselyov algorithms generate code that is significantly smaller than optimized versions of classic bracket abstraction.
262
+
But what about performance? Is the code generated by the Kiselyov algorithms also faster?
263
+
264
+
To answer this question i have implemented a simple benchmarking suite based on the [micro-benchmarking framework Criterion](http://www.serpentine.com/criterion/).
265
+
266
+
In my suite I am testing the performance of combinations of the following components:
267
+
268
+
- the compilers `compileBracket`, `compileEta` and `compileBulk` from the previous section
269
+
- the function factorial, fibonacci, ackermann and tak from the previous section
270
+
- the execution backenda Graph Reduction Engine and the native Haskell functions implementaion from my previous post
0 commit comments