diff options
| author | Marvin Borner | 2024-02-16 16:46:45 +0100 |
|---|---|---|
| committer | Marvin Borner | 2024-02-16 16:56:55 +0100 |
| commit | f3dc81930ebbc6727f9a796f71dceffbcb753752 (patch) | |
| tree | 01dc563ac42b5d45091a4adc180e016078d38091 /std/Number | |
| parent | a852b3e28f7f080c1912e9a7c07cb85636bce89a (diff) | |
Added strong Rosenberg encoding for meta encoding
Originally got the idea from @sgoguen (YC) and was further inspired by
@hbr from one of their blog posts[1].
The current encoding has some holes and bad performance, so I might
switch to a different one in the future.
The wiki and metaprogramming blog post have been updated accordingly.
[1] https://hbr.github.io/Lambda-Calculus/computability/text.html
Diffstat (limited to 'std/Number')
| -rw-r--r-- | std/Number/Conversion.bruijn | 1 | ||||
| -rw-r--r-- | std/Number/Pairing.bruijn | 24 |
2 files changed, 25 insertions, 0 deletions
diff --git a/std/Number/Conversion.bruijn b/std/Number/Conversion.bruijn index ff08f89..c9a568f 100644 --- a/std/Number/Conversion.bruijn +++ b/std/Number/Conversion.bruijn @@ -1,3 +1,4 @@ +# MIT License, Copyright (c) 2024 Marvin Borner # convert bases to other bases :import std/Number/Unary U diff --git a/std/Number/Pairing.bruijn b/std/Number/Pairing.bruijn new file mode 100644 index 0000000..a3a7e4a --- /dev/null +++ b/std/Number/Pairing.bruijn @@ -0,0 +1,24 @@ +# MIT License, Copyright (c) 2024 Marvin Borner +# pairing functions for writing two integers as one, bijectionally + +:import std/Logic . +:import std/Pair . +:import std/Number . +:import std/Math . + +# strong Rosenberg pairing function +pair-ternary [[[0 ⋅ 0 + 0 + 2 - 1] (max 1 0)]] ⧗ Number → Number → Number + +:test ((pair-ternary (+0) (+0)) =? (+0)) (true) +:test ((pair-ternary (+0) (+1)) =? (+1)) (true) +:test ((pair-ternary (+1) (+0)) =? (+3)) (true) +:test ((pair-ternary (+2) (+1)) =? (+7)) (true) + +# strong Rosenberg unpairing function +unpair-ternary [[[go] (1 - (0 ⋅ 0))] (sqrt 0)] ⧗ Number → (Pair Number Number) + go (0 <? 1) (0 : 1) (1 : (1 ⋅ 1 + 1 + 1 - 2)) + +:test (strip <$> (unpair-ternary (+0))) ((+0) : (+0)) +:test (strip <$> (unpair-ternary (+1))) ((+0) : (+1)) +:test (strip <$> (unpair-ternary (+3))) ((+1) : (+0)) +:test (strip <$> (unpair-ternary (+7))) ((+2) : (+1)) |