blob: 51ae178a013529f5691c64c19eafb72e1031a040 (
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
25
26
27
28
29
30
31
32
33
|
# MIT License, Copyright (c) 2024 Marvin Borner
# see "on the representation of data in lambda-calculus" (Parigot 1989)
# has a "one-step" predecessor *and* addition function
# zero Parigot number
zero [0] ⧗ Parigot
# increments Parigot number
inc [[[0 (2 1)]]] ⧗ Parigot → Parigot
++‣ inc
# decrements Parigot number
dec [[1 0 [0]]] ⧗ Parigot → Parigot
--‣ dec
:test (dec (inc zero)) (zero)
# adds two Parigot numbers
add [[[2 (1 0)]]] ⧗ Parigot → Parigot → Parigot
…+… add
:test (add (inc (zero)) (inc (inc zero))) (inc (inc (inc zero)))
iter [[[0 ι ρ ρ]]]
ρ [[3 (1 0 0)]]
ι [[4]]
rec [[[0 ι ρ ρ --0]]]
ρ [[[4 0 (2 1 1)]]]
ι [[[5]]]
|
