blob: 9a23fd4009d8bb4f554c722992bfcb8ca759b866 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
# MIT License, Copyright (c) 2024 Marvin Borner
# see "on the representation of data in lambda-calculus" #5
# has a "one-step" predecessor *and* addition function
# has 2x space complexity compared to unary/Church
zero [0]
inc [[[0 2 1]]]
++‣ inc
dec [[1 0 [0]]]
--‣ dec
:test (dec (inc zero)) (zero)
iter [[[0 ι ρ ρ]]]
ρ [[3 (1 0 0)]]
ι [[4]]
rec [[[0 ι ρ ρ --0]]]
ρ [[[4 0 (2 1 1)]]]
ι [[[5]]]
|
