diff options
| author | Marvin Borner | 2024-08-02 00:26:21 +0200 |
|---|---|---|
| committer | Marvin Borner | 2024-08-02 00:26:21 +0200 |
| commit | e2c3965f929556dda9f779c237f4ba96c8f6c542 (patch) | |
| tree | 208d981f6b9bd1829a99bce8ea3a55671e08a2fd /std/Number | |
| parent | 8d8c22cefbcb4a108adc20f46a2dcae67ec8b6c6 (diff) | |
Improved Parigot data types
Diffstat (limited to 'std/Number')
| -rw-r--r-- | std/Number/Parigot.bruijn | 19 |
1 files changed, 14 insertions, 5 deletions
diff --git a/std/Number/Parigot.bruijn b/std/Number/Parigot.bruijn index 9a23fd4..51ae178 100644 --- a/std/Number/Parigot.bruijn +++ b/std/Number/Parigot.bruijn @@ -1,20 +1,29 @@ # MIT License, Copyright (c) 2024 Marvin Borner -# see "on the representation of data in lambda-calculus" #5 +# see "on the representation of data in lambda-calculus" (Parigot 1989) # has a "one-step" predecessor *and* addition function -# has 2x space complexity compared to unary/Church -zero [0] +# zero Parigot number +zero [0] ⧗ Parigot -inc [[[0 2 1]]] +# increments Parigot number +inc [[[0 (2 1)]]] ⧗ Parigot → Parigot ++‣ inc -dec [[1 0 [0]]] +# 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]] |