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

1 files changed, 30 insertions, 0 deletions

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]]