7 files changed, 109 insertions, 1 deletions

diff --git a/bruijn.cabal b/bruijn.cabal
index c77f148..0e16f9d 100644
--- a/bruijn.cabal
+++ b/bruijn.cabal
@@ -22,6 +22,7 @@ data-files:
     std/Char.bruijn
     std/Combinator.bruijn
     std/Float.bruijn
+    std/gen_all.sh
     std/List.bruijn
     std/Logic.bruijn
     std/Math.bruijn
@@ -35,6 +36,8 @@ data-files:
     std/String.bruijn
     std/AIT/Beavers.bruijn
     std/Number/Binary.bruijn
+    std/Number/Conversion.bruijn
+    std/Number/Pairing.bruijn
     std/Number/Ternary.bruijn
     std/Number/Unary.bruijn
     std/Tree/Balanced.bruijn
diff --git a/docs/wiki_src/coding/meta-programming.md b/docs/wiki_src/coding/meta-programming.md
index 334e285..716cc7a 100644
--- a/docs/wiki_src/coding/meta-programming.md
+++ b/docs/wiki_src/coding/meta-programming.md
@@ -74,4 +74,12 @@ Examples:
 :test (map inc `0) (`1)
 :test (map (map inc) `[0]) (`[1])
 :test (map swap `[0 1]) (`[1 0])
+
+# encoding terms as numbers
+:test ((encode `(0 0)) =? (+3)) (true)
+:test ((encode `[0]) =? (+8)) (true)
+
+# decoding numbers to terms
+:test (decode (+3)) (`(0 0))
+:test (decode (+8)) (`[0])
 ```
diff --git a/samples/fun/encode.bruijn b/samples/fun/encode.bruijn
new file mode 100644
index 0000000..75204b9
--- /dev/null
+++ b/samples/fun/encode.bruijn
@@ -0,0 +1,30 @@
+# encode lambda terms as numbers
+# from https://hbr.github.io/Lambda-Calculus/computability/text.html
+# see also std/Meta for unary variant
+
+:import std/Combinator .
+:import std/Logic .
+:import std/Math .
+
+# compute pairing function [n,m]
+compress [[--((pow (+2) 1) ⋅ ++((+2) ⋅ 0))]] ⧗ Number → Number → Number
+
+:test ((compress (+0) (+0)) =? (+0)) (true)
+:test ((compress (+1) (+0)) =? (+1)) (true)
+:test ((compress (+0) (+1)) =? (+2)) (true)
+:test ((compress (+2) (+1)) =? (+11)) (true)
+
+idx compress (+0) ⧗ Number → Number
+
+app (compress (+1)) ∘∘ compress ⧗ Number → Number → Number
+
+abs (compress (+2)) ∘∘ compress ⧗ Number → Number → Number
+
+enc_zero abs (+1) (abs (+0) (idx (+0))) ⧗ Number
+
+enc_inc abs (+2) (abs (+1) (abs (+0) enc)) ⧗ Number
+	enc app (idx (+1)) (app (app (idx (+2)) (idx (+1))) (idx (+0)))
+
+wrap [0 (app enc_inc) enc_zero] ⧗ Number → Number
+
+main [[0]]
diff --git a/std/Math.bruijn b/std/Math.bruijn
index 1737572..ec358fe 100644
--- a/std/Math.bruijn
+++ b/std/Math.bruijn
@@ -1,5 +1,5 @@
 # MIT License, Copyright (c) 2022 Marvin Borner
-# experimental functions, sometimes list-based
+# experimental functions; sometimes list-based; could work on any base
 
 :input std/Number
 
@@ -123,6 +123,18 @@ fib [fibs !! ++0] ⧗ Number
 
 :test (fib (+5)) ((+8))
 
+# floored integer square root using Babylonian method
+sqrt [z [[[[rec]]]] (+1) 0 0] ⧗ Number → Number
+	rec (1 >? 2) case-rec case-end
+		case-rec [4 (1 / 0) 0 1] /²(2 + 1)
+		case-end 1
+
+:test ((sqrt (+0)) =? (+0)) (true)
+:test ((sqrt (+1)) =? (+1)) (true)
+:test ((sqrt (+2)) =? (+1)) (true)
+:test ((sqrt (+5)) =? (+2)) (true)
+:test ((sqrt (+9)) =? (+3)) (true)
+
 # integer logarithm
 log z [[[[rec]]]] (+1) ⧗ Number → Number → Number
 	rec [((3 ≤? 1) ⋀? (1 <? 0)) case-end case-rec] (2 ⋅ 1)
diff --git a/std/Meta.bruijn b/std/Meta.bruijn
index 31d781a..3b67c35 100644
--- a/std/Meta.bruijn
+++ b/std/Meta.bruijn
@@ -5,6 +5,8 @@
 :import std/Combinator .
 :import std/Number/Unary .
 :import std/List .
+:import std/Number/Pairing .
+:import std/Number/Conversion .
 :import std/Pair P
 
 # constructor of meta abstraction
@@ -223,3 +225,31 @@ map [[0 case-idx case-app case-abs]] ⧗ (Meta → Meta) → Meta → Meta
 :test (map swap `[0 1]) (`[1 0])
 :test (map inc `0) (`1)
 :test (map (map inc) `[0]) (`[1])
+
+# ternary encoding of meta terms
+# inspired by Helmut Brandl's and Steve Goguen's work
+# uses ternary for lower space complexity
+encode fold idx-cb app-cb abs-cb ⧗ Meta → Number
+	idx-cb (pair-ternary (+0)) ∘ unary-to-ternary
+	app-cb (pair-ternary (+1)) ∘∘ pair-ternary
+	abs-cb pair-ternary (+2)
+
+:test (ternary-to-unary (encode `0)) ((+0u))
+:test (ternary-to-unary (encode `1)) ((+1u))
+:test (ternary-to-unary (encode `(0 0))) ((+3u))
+:test (ternary-to-unary (encode `[1])) ((+7u))
+:test (ternary-to-unary (encode `[0])) ((+8u))
+
+# decode ternary encoding back to meta term
+# TODO: improve performance (maybe with different unpairing function or better sqrt)
+decode z [[unpair-ternary 0 go]] ⧗ Number → Meta
+	go [[(case-idx : (case-app : {}case-abs)) !! 1 0]]
+		case-idx idx ∘ ternary-to-unary
+		case-app [unpair-ternary 0 (ψ app 4)]
+		case-abs abs ∘ 3
+
+:test (decode (+0)) (`0)
+:test (decode (+1)) (`1)
+:test (decode (+3)) (`(0 0))
+:test (decode (+7)) (`[1])
+:test (decode (+8)) (`[0])
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))