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
|
# calm
> **c**alm **a**bstract **l**ambda **m**achine
- **Strong** reduction (reduction inside abstractions) of
**call-by-need** lambda calculus
- Originally intended as reducer of the
[`bruijn`](https://github.com/marvinborner/bruijn) programming
language
- Useful for proof assistants or as a high-level lambda-term reducer
of functional programming languages
- Based on bleeding-edge research results
- Exponentially big normal forms of the family $e_n=λx.c_nωx$, where
$ω:=λx.xx$ and $c_n$ denotes the $n$th Church numeral, consume only
a linear in $n$ amount of memory and are computed in linear
time\[0\]
## Why C?
You might realize that the reduction transitions are of a very
functional nature and aren't that obvious to implement in non-functional
languages.
I used C because **(1)** most functional languages use automatic memory
management (often using periodic garbage collecting) which unnecessarily
slows down the transitions, **(2)** there aren't that many efficient
lambda calculus reducers in C out there, **(3)** it's a fun challenge
and **(4)** I like C.
## Libraries
- [CHAMP](https://github.com/ammut/immutable-c-ollections) \[MIT\]:
Underrated efficient hash array mapped trie
## Research
Interesting/relevant research in no particular order:
0. Biernacka, M., Charatonik, W., & Drab, T. (2022). A simple and
efficient implementation of strong call by need by an abstract
machine. Proceedings of the ACM on Programming Languages, 6(ICFP),
109-136.
1. Accattoli, B., Condoluci, A., & Coen, C. S. (2021, June). Strong
call-by-value is reasonable, implosively. In 2021 36th Annual
ACM/IEEE Symposium on Logic in Computer Science (LICS) (pp. 1-14).
IEEE.
2. Balabonski, T., Lanco, A., & Melquiond, G. (2021). A strong
call-by-need calculus. arXiv preprint arXiv:2111.01485.
3. Accattoli, B., Condoluci, A., Guerrieri, G., & Coen, C. S. (2019,
October). Crumbling abstract machines. In Proceedings of the 21st
International Symposium on Principles and Practice of Declarative
Programming (pp. 1-15).
4. Accattoli, B., & Coen, C. S. (2015, July). On the relative
usefulness of fireballs. In 2015 30th Annual ACM/IEEE Symposium on
Logic in Computer Science (pp. 141-155). IEEE.
5. Condoluci, A., Accattoli, B., & Coen, C. S. (2019, October). Sharing
equality is linear. In Proceedings of the 21st International
Symposium on Principles and Practice of Declarative Programming
(pp. 1-14).
6. Accattoli, B., & Leberle, M. (2021). Useful open call-by-need. arXiv
preprint arXiv:2107.06591.
|
