From 5fb4e3f91e8ba77a07c804f7a784a8a7fb1c123f Mon Sep 17 00:00:00 2001 From: Marvin Borner Date: Tue, 12 Sep 2023 00:01:00 +0200 Subject: Documentation --- app/Main.hs | 39 ++++++++++----------- fun/church.txt | 26 ++++++++++++++ readme.md | 95 +++++++++++++++++++++++++++++++++------------------- samples/add.birb | 9 ++--- samples/biology.birb | 2 ++ samples/inc0.birb | 2 ++ samples/inc1.birb | 2 ++ samples/incn.birb | 5 +++ samples/list.birb | 8 +++++ 9 files changed, 130 insertions(+), 58 deletions(-) create mode 100644 fun/church.txt create mode 100644 samples/incn.birb create mode 100644 samples/list.birb 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 + πŸ¦‰ + 🦜 + πŸ¦… + πŸͺ½ + 🦚 -- cgit v1.2.3