Documentation

author: Marvin Borner 2023-09-12 00:01:00 +0200
committer: Marvin Borner 2023-09-12 00:01:25 +0200
commit: 5fb4e3f91e8ba77a07c804f7a784a8a7fb1c123f (patch)
tree: 643aea5387f2901f3e45357d36fbb5cc15b6e679
parent: 4f8619571a4ec823b020baf9bc11f76fb706897e (diff)
9 files changed, 130 insertions, 58 deletions
diff --git a/app/Main.hs b/app/Main.hs
index 68c08fd..3509c47 100644
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -73,19 +73,20 @@ subst i (Abs a  ) c = Abs (subst (i + 1) a (shift 0 c))
 
 nf :: Term -> IO Term
 nf o = do -- TODO: pointfree??
-  i <- newIORef 1000
+  -- i <- newIORef 1000
+  i <- newIORef 100000000
   go i o
  where
   go :: IORef Integer -> Term -> IO Term
   go i t = do -- oracle
     readIORef i >>= \case
-      0    -> writeIORef i (-1) >> return (Idx 0)
-      -- 0 -> do
-      --   putStrLn "💥 potential infinite loop, continue? [yn]"
-      --   getLine >>= \case
-      --     "y" -> writeIORef i (-2) >> re i t
-      --     "n" -> writeIORef i (-1) >> return t
-      --     _   -> go i t
+      -- 0    -> writeIORef i (-1) >> return (Idx 0)
+      0 -> do
+        putStrLn "💥 potential infinite loop, continue? [yn]"
+        getLine >>= \case
+          "y" -> writeIORef i (-2) >> re i t
+          "n" -> writeIORef i (-1) >> return t
+          _   -> go i t
       (-1) -> return t
       _    -> modifyIORef i (subtract 1) >> re i t
 
@@ -122,17 +123,17 @@ bruteForce s n =
   in  putStrLn ("trying " ++ show n) >> go termified
 
 main :: IO ()
-main = mapM_ (bruteForce "!!@1@1@1@1@10") [1 .. 10]
--- main = do
---   args <- getArgs
---   file <- readFile (head args)
---   let termified   = fromBirbs file
---   let rebirbified = fromTerm termified
---   putStrLn $ "input: " ++ rebirbified
---   normalBirbs <- nf termified
---   let retermified = fromTerm normalBirbs
---   putStrLn $ "reduced: " ++ retermified
---   return ()
+-- main = mapM_ (bruteForce "...") [1 .. 10]
+main = do
+  args <- getArgs
+  file <- readFile (head args)
+  let termified   = fromBirbs file
+  let rebirbified = fromTerm termified
+  putStrLn $ "input: " ++ rebirbified
+  normalBirbs <- nf termified
+  let retermified = fromTerm normalBirbs
+  putStrLn $ "reduced: " ++ retermified
+  return ()
 
 -- this isn't really relevant but I'm too lazy to type the terms manually
 parse :: String -> Term
diff --git a/fun/church.txt b/fun/church.txt
new file mode 100644
index 0000000..4c9dd5e
--- /dev/null
+++ b/fun/church.txt
@@ -0,0 +1,26 @@
+The smallest birb code that reduces to Church numeral n:
+
+0: 2 birbs
+🐥🐦
+🦩🐥
+🦢🐥
+
+1: 2 birbs
+🦚🐦
+🐧🐦
+
+2: 3 birbs
+🦢🦚🐦
+🦢🐧🐦
+
+3: 6 birbs
+🦜🦩🕊🦢🦚🐦
+🦜🦩🕊🦢🐧🐦
+🦜🦩🦉🦢🐧🐦
+🦜🦩🪽🦢🕊🐦
+
+4: 4 birbs
+🦜🦢🦚🐦
+🦜🦢🐧🐦
+
+...
diff --git a/readme.md b/readme.md
index c64fd84..9023b61 100644
--- a/readme.md
+++ b/readme.md
@@ -10,23 +10,23 @@ lambda calculus.
 Unfortunately, the Unicode standard does not yet have many
 (single-character) birds. These are the ones currently mapped/supported:
 
-| emoji | animal         | combinator   | bruijn              | term                               |
-|:-----:|----------------|--------------|---------------------|------------------------------------|
-|  🦉   | owl            | owl          | `[[0(10)]]`         | $\lambda ab.b(ab)$                 |
-|  🦅   | eagle          | eagle        | `[[[[[43(210)]]]]]` | $\lambda abcde.ab(cde)$            |
-|  🪽   | wing           | phoenix      | `[[[[3(20)(10)]]]]` | $\lambda abcd.a(bd)(cd)$           |
-|  🕊️   | dove           | dove         | `[[[[32(10)]]]]`    | $\lambda abcd.ab(cd)$              |
-|  🦜   | parrot         | mockingbird  | `[00]`              | $\lambda a.aa$                     |
-|  🦆   | duck           | quacky       | `[[[0(12)]]]`       | $\lambda abc.c(ba)$                |
-|  🐤   | touring chick  | turing       | `[[0(110)]]`        | $\lambda ab.b(aab)$                |
-|  🐥   | kool chick     | kestrel      | `[[1]]`             | $\lambda ab.a$                     |
-|  🐣   | hatching chick | quirky       | `[[[0(21)]]]`       | $\lambda abc.c(ab)$                |
-|  🐦   | simple bird    | identity     | `[0]`               | $\lambda a.a$                      |
-|  🦚   | peacock        | queer        | `[[[1(20)]]]`       | $\lambda abc.b(ac)$                |
-|  🦤   | dodo           | sage         | `[[0(11)][0(11)]]`  | $\lambda ab.b(aa)\lambda ab.b(aa)$ |
-|  🐧   | penguin        | blackbird    | `[[[2(10)]]]`       | $\lambda abc.a(bc)$                |
-|  🦢   | swan           | substitution | `[[[20(10)]]]`      | $\lambda abc.ac(bc)$               |
-|  🦩   | flamingo       | cardinal     | `[[[201]]]`         | $\lambda abc.acb$                  |
+| emoji | animal         | combinator   | term                               |
+|:-----:|----------------|--------------|------------------------------------|
+|  🦉   | owl            | owl          | $\lambda ab.b(ab)$                 |
+|  🦅   | eagle          | eagle        | $\lambda abcde.ab(cde)$            |
+|  🪽   | wing           | phoenix      | $\lambda abcd.a(bd)(cd)$           |
+|  🕊️   | dove           | dove         | $\lambda abcd.ab(cd)$              |
+|  🦜   | parrot         | mockingbird  | $\lambda a.aa$                     |
+|  🦆   | duck           | quacky       | $\lambda abc.c(ba)$                |
+|  🐤   | touring chick  | turing       | $\lambda ab.b(aab)$                |
+|  🐥   | kool chick     | kestrel      | $\lambda ab.a$                     |
+|  🐣   | hatching chick | quirky       | $\lambda abc.c(ab)$                |
+|  🐦   | simple bird    | identity     | $\lambda a.a$                      |
+|  🦚   | peacock        | queer        | $\lambda abc.b(ac)$                |
+|  🦤   | dodo           | sage         | $\lambda ab.a(bb)\lambda ab.a(bb)$ |
+|  🐧   | penguin        | blackbird    | $\lambda abc.a(bc)$                |
+|  🦢   | swan           | substitution | $\lambda abc.ac(bc)$               |
+|  🦩   | flamingo       | cardinal     | $\lambda abc.acb$                  |
 
 Lonely/unmatched birbs: 🐔🦃🐓
 
@@ -35,10 +35,13 @@ Lonely/unmatched birbs: 🐔🦃🐓
 - `[birb]+`: Birb
 - everything else: Comment
 
+Syntax errors are impossible as long as you use at least one birb.
+
 # Semantics
 
 Birbs stagger as they walk: they are reduced in alternating associative
-order, starting with birb index $\lfloor\frac{\texttt{len}}{2}\rfloor$:
+order, starting with left associativity at birb index
+$\lfloor\frac{\texttt{len}}{2}\rfloor$:
 
     🐦🐦 -> (🐦🐦)
     🐦🐦🐦 -> ((🐦🐦)🐦)
@@ -46,46 +49,65 @@ order, starting with birb index $\lfloor\frac{\texttt{len}}{2}\rfloor$:
     🐦🐦🐦🐦🐦 -> ((🐦((🐦🐦)🐦))🐦)
     🐦🐦🐦🐦🐦🐦 -> (🐦((🐦((🐦🐦)🐦))🐦))
     🐦🐦🐦🐦🐦🐦🐦 -> ((🐦((🐦((🐦🐦)🐦))🐦))🐦)
+    ...
 
 # Examples
 
-You can find more examples in the `samples/` directory.
+You can find more examples (with comments) in the `samples/` directory.
 
 ## Relationships
 
-- 🦉🐦 $\rightsquigarrow$ 🦜
+- 🪽🐦 $\rightsquigarrow$ 🦢
 - 🦢🐦 $\rightsquigarrow$ 🦉
+- 🦉🐦 $\rightsquigarrow$ 🦜
+- 🕊️🐦 $\rightsquigarrow$ 🐧
 - 🐧🐧 $\rightsquigarrow$ 🕊️
 - 🦩🐧 $\rightsquigarrow$ 🦚
 - 🦩🦚 $\rightsquigarrow$ 🐧
+- 🦩🦆 $\rightsquigarrow$ 🐣
 
-One can only imagine what happens if two parrots repeat each other: 🦜🦜
-$\rightsquigarrow$ 💥
+One can only imagine what happens if two parrots talk to each other:
+🦜🦜 $\rightsquigarrow$ 💥. The same happens with 🐤🐤; they just can’t
+stop waddling!
 
 ## Arithmetic
 
 For this example I use the Church numerals. Zero would then be encoded
 as 🐥🐦. The successor function can be written as 🦢🐧:
 
-- 🐦🐧🐦🦢🐧🐥🐦 $\rightsquigarrow$ λλ(10) – (Church numeral 1)
-- 🐦🐧🐦🐧🕊️🦢🐧🦢🐧🐥🐦 $\rightsquigarrow$ λλ(1(10)) – (Church numeral
-  2)  
+- 🐦🐧🐦🦢🐧🐥🐦 $\rightsquigarrow\lambda\lambda(10)$ – (Church numeral
+  1)  
+- 🐦🐧🐦🐧🕊️🦢🐧🦢🐧🐥🐦 $\rightsquigarrow\lambda(1(10))$ – (Church
+  numeral 2)
 
 Similarly, one can very obviously translate the Church addition function
-to 🐧🦢🐥🦢🕊️. Now, to calculate $1+2$ based on their increments from
-zero:
+to 🪽🐧. Now, to calculate $1+2$ based on their increments from zero:
 
-- 🦢🐧🦢🐧🐥🐦
+- 🐦🐦🕊️🐧🕊️🐧🐦🐧🕊️🐧🕊️🪽🐧🦢🐧🦢🐧🐥🐦🦢🐧🐥🐦
+  $\rightsquigarrow\lambda(1(1(10)))$ – (Church numeral 3)
 
 Also: 🐧 is $a\cdot b$, 🦜 is $n^n$ and 🦚🐦 $a^b$.
 
-Note that there are many alternative ways to do arithmetic. Try writing
-the functions above with other birbs!
+Note that there exist many alternative ways to do arithmetic. Try
+writing the functions above with other birbs!
+
+## Containers
+
+You can create a pair $\langle X,Y\rangle$ using `🦩🦩🦩YX`.
+
+Typically, one would now construct a list using repeated application of
+pairs (Boehm-Berarducci/Church encoding). However, due to the reversed
+application and alternating associativity, the Mogensen-Scott encoding
+is more suitable:
+
+List $\langle X_1,X_2,\dots,X_n\rangle$: `[🦩]ⁿ🦩X2X1...XN`.
 
 ## Busy ~~beavers~~ birbs
 
-- The touring eagle: 🐦🐦🐦🦅🐤🦅🐤🦅🐤 (~20M BLC bits)
-- more? PR!
+Contestants:
+
+- *The touring eagle*: `[🐦]ⁿ[🦅🐤]ⁿ` ($n=3$: 9 birbs, ~20M BLC bits)
+- better? PR!
 
 # Usage
 
@@ -102,9 +124,12 @@ sometimes manually converted the term back to birbs.
 
 # Turing-completeness
 
-The language is probably Turing complete. If the language supported
-left- *and* right-associativity, 🐧 would be enough to prove its
-completeness.
+Birb is Turing complete.
+
+It turns out that even its sub-language $\Sigma=\{🦢🐥\}$ (SK) is Turing
+complete, since the semantics allow an initial construction of 🐦 using
+`((🦢 🐥) 🐥)`. By doing that, birb is equivalent to the
+[Jot](https://esolangs.org/wiki/Jot) variant of Iota calculus.
 
 ------------------------------------------------------------------------
 
diff --git a/samples/add.birb b/samples/add.birb
index fc11d4f..058f92f 100644
--- a/samples/add.birb
+++ b/samples/add.birb
@@ -1,7 +1,8 @@
-
-
-🐦🐦🐦🐧🦢🐥🦢🕊️ add ...
-  🐦🐧🐦🐧🕊️ wrapper for two
+🐦🐦🕊️🐧🕊️ wrapper for `1+(++0)`
+  🐧🐦🐧🕊️🐧🕊️ wrapper for `add ++(++0)`
+    🪽🐧 add
     🦢🐧 inc
       🦢🐧 inc
         🐥🐦 zero
+  🦢🐧 inc
+    🐥🐦 zero
diff --git a/samples/biology.birb b/samples/biology.birb
index fa2259a..b71abc8 100644
--- a/samples/biology.birb
+++ b/samples/biology.birb
@@ -1,2 +1,4 @@
 construct list
+🐧🦩
+
 🦩🦚
diff --git a/samples/inc0.birb b/samples/inc0.birb
index d9d227c..8245721 100644
--- a/samples/inc0.birb
+++ b/samples/inc0.birb
@@ -1,6 +1,8 @@
+decoded:
    (s b) (k i)
 -> ((i ((b ((i s) b)) k)) i)
 
+encoded:
 🐦🐧🐦 wrapper
   🦢🐧 inc
     🐥🐦 zero
diff --git a/samples/inc1.birb b/samples/inc1.birb
index 656250c..44683c5 100644
--- a/samples/inc1.birb
+++ b/samples/inc1.birb
@@ -1,7 +1,9 @@
+decoded:
    b (s b) (s b) (k i)
 -> (i ((i ((b ((d s) b)) s)) b)) (k i)
 -> ((i ((b ((i ((b ((d s) b)) s)) b)) k)) i)
 
+encoded:
 🐦🐧🐦🐧🕊️ wrapper
   🦢🐧 inc
     🦢🐧 inc
diff --git a/samples/incn.birb b/samples/incn.birb
new file mode 100644
index 0000000..a8c5c78
--- /dev/null
+++ b/samples/incn.birb
@@ -0,0 +1,5 @@
+TODO: Find more general way of incrementing
+🐦🐧🐦🐧 wrapper
+  🐦🦢🐧 inc
+    🦢🐧 inc
+      🐥🐦 zero
diff --git a/samples/list.birb b/samples/list.birb
new file mode 100644
index 0000000..04ec539
--- /dev/null
+++ b/samples/list.birb
@@ -0,0 +1,8 @@
+Mogensen-Scott encoding
+
+🦩🦩🦩🦩🦩🦩 list with 5 elements
+  🦉
+  🦜
+  🦅
+  🪽
+  🦚
author	Marvin Borner	2023-09-12 00:01:00 +0200
committer	Marvin Borner	2023-09-12 00:01:25 +0200
commit	5fb4e3f91e8ba77a07c804f7a784a8a7fb1c123f (patch)
tree	643aea5387f2901f3e45357d36fbb5cc15b6e679
parent	4f8619571a4ec823b020baf9bc11f76fb706897e (diff)