From d22c013e4e74889a82004b05aab1158b98cfafc9 Mon Sep 17 00:00:00 2001 From: Marvin Borner Date: Thu, 14 Dec 2023 20:14:49 +0100 Subject: [PATCH] Minor documentation fixes --- docs/code.js | 2 +- docs/index.html | 254 ++++++++++++++---------- docs/script.js | 8 +- docs/style.css | 72 +++++-- docs/wiki_src/coding/data-structures.md | 4 + docs/wiki_src/coding/mixfix.md | 3 +- docs/wiki_src/technical/performance.md | 2 +- readme.md | 21 ++ std/List.bruijn | 4 +- std/Math.bruijn | 1 + std/Number.bruijn | 2 +- std/Number/Binary.bruijn | 1 + std/Number/Ternary.bruijn | 3 +- std/Tree/Rose.bruijn | 4 +- 14 files changed, 246 insertions(+), 135 deletions(-) diff --git a/docs/code.js b/docs/code.js index 3a2a7bd..0384eca 100644 --- a/docs/code.js +++ b/docs/code.js @@ -10,7 +10,7 @@ const term = (t) => .replaceAll(/(\))(?!\<)/g, ")") .replaceAll("[", "[") .replaceAll("]", "]") - .replaceAll(/(?$1"); + .replaceAll(/(?$1"); const highlightTerm = (elem) => { elem.innerHTML = term(elem.innerHTML); diff --git a/docs/index.html b/docs/index.html index deb1d92..a66c96c 100644 --- a/docs/index.html +++ b/docs/index.html @@ -1,134 +1,188 @@ - + - - - - - - bruijn programming language - - -
- -

bruijn

-
- -
- 
-pow […!!… (iterate (…⋅… 0) (+1))]
+  
+    
+    
+    
+    
+    bruijn programming language
+  
+  
+    

+      
+      
bruijn

+    

+
+    

+      

+        
+pow [index (iterate (mul 0) (+1))]
 
 …**… pow
 
 :test ((+2) ** (+3) =? (+8)) (true)

-			
-			

-				Functional language based on pure bruijn-indexed lambda calculus.
-			

-		

-
-		

-			Hint: Click on anything you don't understand.
-		

-
-		

-			

-				Lambdas all the way down.

-				No primitive functions.
-			

-			
+      

+
+      

+        

+          Functional programming language based on pure De Bruijn indexed lambda
+          calculus.
+        

+      

+    

+
+    

+      Hint: Click on anything you don't understand.
+    

+
+    

+      

+        

+          Lambdas all the way down.

+          No primitive functions.
+        

+      

+      

+        
 > (+5)
 [[[[2 (2 (1 3))]]]]
 > 'a'
 [[[1 (0 (0 (0 (0 (1 (1 (0 2)))))))]]]
 > add
 [[(([([[1 0 [[0]]]] ((((0 [[(((0...

-		

+      

 
-		

-			
+      

+        
 > :time factorial (+30)
 0.15 seconds

-			

-				Efficient call-by-need reduction using abstract machines.
-			

-		

-
-		

-			

-				Substantial standard library.

-				Source
-			

-			
+      

+      

+        
Efficient call-by-need reduction using abstract machines.

+      

+
+      

+        

+          Substantial standard library.

+          Source
+        

+      

+      

+        
 > ∏ (+1) → (+3) | ++‣
 > number! <$> (lines "42\n25")
 > sum (take (+3) (repeat (+4)))
 > (+10b) ⋀! (+12b)

-		

+      

 
-		

-			
+      

+        
 $ echo "main [0]" > echo.bruijn
 $ bruijn -b echo.bruijn > echo
 $ wc -c echo
 2 echo
 $ echo "hello world!" | bruijn -e echo
-hello world!

-			

-				Compilation to Tromp's binary lambda calculus.

-				Support for byte and ASCII encoding.
-			

-		

-
-		

-            Learn more: Wiki, Std
-		

-
-		

-			
Installation

-			
+hello world!

+      

+      

+        

+          Compilation to Tromp's binary lambda calculus.

+          Support for byte and ASCII encoding.
+        

+      

+    

+
+    

+      Learn more: Wiki, Std
+    

+
+    

+      
Installation

+      
 $ git clone https://github.com/marvinborner/bruijn.git && cd bruijn
 $ stack run # for playing around
 $ stack install
-$ bruijn
	
-		

+$ bruijn
+
-
-

Broogle

- 
+    

+      
Broogle

+      
 $ ./broogle.sh -f add
 add ⧗ Unary → Unary → Unary
 also known as …+…
 in std/Number/Unary.bruijn:35
 # adds two unary numbers
-...
	
-		

-
-		

-			
Why?

-			
    
-				
  • Compiled binary lambda calculus is incredibly expressive and tiny. Read the articles by Justine and Tromp.
    • 
-				
  • Exploring different encodings of data as function abstractions is fascinating.
    • 
-				
  • Pure lambda calculus can be very beautiful. You will understand if you try to have some fun with it.
    • 
-				
  • I don't like naming parameters of functions. Using bruijn indices is a universal reference independent of the function and can actually help readability if you're familiar enough.
    • 
-				
  • Really, just for fun.
    • 
-			

-		

-
-		

-			
Articles

-			
-		

-
-		

-			Open-source: GitHub
-		

-
-		
-	
+...
+
+ +
+

Why?

+ +
+ +
+

Articles

+ +
+ +
+ Open-source: GitHub +
+ + + diff --git a/docs/script.js b/docs/script.js index 21f0cdf..5859c55 100644 --- a/docs/script.js +++ b/docs/script.js @@ -29,12 +29,12 @@ const describe = (c, d) => { [...document.getElementsByClassName(c)].forEach(el => el.addEventListener("click", e => notify(d, e))); } -describe("binary", "Syntactic sugar for a binary number representation using abstractions as data. Needs a sign and brackets to differentiate it from bruijn indices"); +describe("binary", "Syntactic sugar for a binary number representation using abstractions as data. Needs a sign and brackets to differentiate it from De Bruijn indices"); describe("char", "Syntactic sugar for a binary representation of characters using abstractions as data."); describe("com", "This indicates a command to the interpreter. The most common commands are :test (verifying α-equivalency) and :import (importing definitions from other files)."); -describe("def", "This defines a new term substitution."); +describe("def", "This defines a new term substitution. Using this identifier will substitute the term on its right side."); describe("header", "[0] is the identity operation. It returns the first argument it gets. Nothing more."); -describe("index", "These numbers reference the nth abstraction, starting counting from the inside. These 'bruijn indices' replace the concept of variables in lambda calculus."); +describe("index", "This number references the nth abstraction, starting counting from the inside. These 'De Bruijn indices' replace the concept of variables in lambda calculus."); describe("left-abs", "The opening bracket of a function abstraction. It's basically the equivalent of the λ in lambda calculus."); describe("left-app", "The opening bracket of a function application."); describe("mixfix", "This is a mixfix operator. They can be defined like …*… where the … can then be any other term. You can use them without the … as a notation of function application."); @@ -44,7 +44,7 @@ describe("right-app", "The closing bracket of a function application."); describe("stack", "Stack is a dependency manager for Haskell. Install it using the corresponding instructions for your operating system.") describe("string", "Syntactic sugar for a list of binary encoded chars.") describe("symbol", "This substitutes a previously defined term (for example from the standard library)."); -describe("ternary", "Syntactic sugar for a balanced ternary number representation using abstractions as data. Needs a sign and brackets to differentiate it from bruijn indices."); +describe("ternary", "Syntactic sugar for a balanced ternary number representation using abstractions as data. Needs a sign and brackets to differentiate it from De Bruijn indices."); describe("time", "Incredibly fast for lambda calculus standards."); document.body.addEventListener("click", clearPopups, true) diff --git a/docs/style.css b/docs/style.css index d986c71..1739f58 100644 --- a/docs/style.css +++ b/docs/style.css @@ -34,22 +34,31 @@ a { .example { display: flex; + flex-flow: row wrap; align-items: center; justify-content: center; - flex-flow: row wrap; - column-gap: 5vw; - max-width: 80%; margin: 0 auto; + width: 50%; +} + +.example > * { + display: flex; + flex-basis: 50%; + justify-content: center; +} + +.example .code { + width: fit-content; } .example p { font-size: 1.2em; - max-width: 80vw; + max-width: 80%; text-align: center; } .instructions { - max-width: 80%; + max-width: 70%; margin: 0 auto; } @@ -59,30 +68,54 @@ a { } } -@media(min-width: 768px) { - .example { - flex-flow: row nowrap; - max-width: 80%; +/* mobile */ +@media(max-width: 768px) { + .example > * { + flex-basis: 100%; } - .example p { - width: 30vw; + .example * { + max-width: 90% !important; + } + + .example { font-size: 1.3em; + width: 100% } .instructions { - max-width: 80%; + max-width: 90%; + font-size: 1.1em; } + + .instructions a { + line-height: 1.5em; + } + + .example :nth-child(8) { order: 7; } + .example :nth-child(7) { order: 8; } + .example :nth-child(6) { order: 6; } + .example :nth-child(5) { order: 5; } + .example :nth-child(4) { order: 3; } + .example :nth-child(3) { order: 4; } + .example :nth-child(2) { order: 2; } + .example :nth-child(1) { order: 1; } } -@media(min-width: 1800px) { +/* small desktop / tablet */ +@media(max-width: 1700px) { .example { - flex-flow: row nowrap; - max-width: 45%; + width: 80%; } - .instructions { - max-width: 35%; + .example .code { + font-size: 1em; + } +} + +@media(max-width: 1000px) { + .example { + width: 100%; } } @@ -124,10 +157,7 @@ a { padding: 15px; font-size: 1.2em; border-radius: 10px; -} - -.instructions .code { - overflow-x: scroll; + overflow: scroll; } .code .repl { diff --git a/docs/wiki_src/coding/data-structures.md b/docs/wiki_src/coding/data-structures.md index 3d2a387..e59fa99 100644 --- a/docs/wiki_src/coding/data-structures.md +++ b/docs/wiki_src/coding/data-structures.md @@ -60,6 +60,10 @@ a-box <>'a' :test (store! a-box 'b') (<>'b') ``` +Options ([`std/Option`](/std/Option.bruijn.html)) use the same data +structure and have additional definitions to resemble Haskell's +`Maybe`{.haskell}. + ## Pairs [`std/Pair`](/std/Pair.bruijn.html) Pairs (tuples) can store any two terms. Pairs can be constructed using diff --git a/docs/wiki_src/coding/mixfix.md b/docs/wiki_src/coding/mixfix.md index d0838cf..43e2100 100644 --- a/docs/wiki_src/coding/mixfix.md +++ b/docs/wiki_src/coding/mixfix.md @@ -41,8 +41,7 @@ chain is not actually overwritten by *another* mixfix chain. ``` bruijn :test ((+8) + (-4) ⋅ (-2)) ((-8)) -# (don't do this) -…+…⋅… [[[(+16)]]] +…+…⋅… [[[2 + (1 ⋅ 0)]]] :test ((+8) + (-4) ⋅ (-2)) ((+16)) ``` diff --git a/docs/wiki_src/technical/performance.md b/docs/wiki_src/technical/performance.md index 05fd683..002a6b8 100644 --- a/docs/wiki_src/technical/performance.md +++ b/docs/wiki_src/technical/performance.md @@ -6,7 +6,7 @@ an extension, bruijn also suffers from bad performance. Bruijn's interpreter works by substituting the entire program into one huge lambda calculus term that will then get reduced by the [reducer](reduction.md). As a result, many equivalent terms get -evaluated multiple times (although some of this get's solved by bruijn's +evaluated multiple times (although some of this is solved by bruijn's call-by-need reduction strategy). We currently work on a solution that reduces all equivalent terms as one, which turns out is not actually that trivial. Follow the [blog](https://text.marvinborner.de) to keep up diff --git a/readme.md b/readme.md index a456752..01d9d7e 100644 --- a/readme.md +++ b/readme.md @@ -33,3 +33,24 @@ Wiki, docs, articles, examples and more: Learn anything about bruijn in the [wiki](https://bruijn.marvinborner.de/wiki/) (also found in `docs/wiki_src/`). + +## References + +0. De Bruijn, Nicolaas Govert. “Lambda calculus notation with nameless + dummies, a tool for automatic formula manipulation, with application + to the Church-Rosser theorem.” Indagationes Mathematicae + (Proceedings). Vol. 75. No. 5. North-Holland, 1972. +1. Mogensen, Torben. “An investigation of compact and efficient number + representations in the pure lambda calculus.” International Andrei + Ershov Memorial Conference on Perspectives of System Informatics. + Springer, Berlin, Heidelberg, 2001. +2. Wadsworth, Christopher. “Some unusual λ-calculus numeral systems.” + (1980): 215-230. +3. Tromp, John. “Binary lambda calculus and combinatory logic.” + Randomness and Complexity, from Leibniz to Chaitin. 2007. 237-260. +4. Tromp, John. “Functional Bits: Lambda Calculus based Algorithmic + Information Theory.” (2022). +5. Biernacka, M., Charatonik, W., & Drab, T. (2022). A simple and + efficient implementation of strong call by need by an abstract + machine. Proceedings of the ACM on Programming Languages, 6(ICFP), + 109-136. diff --git a/std/List.bruijn b/std/List.bruijn index 39aecf8..bb8bed3 100644 --- a/std/List.bruijn +++ b/std/List.bruijn @@ -1,7 +1,6 @@ # MIT License, Copyright (c) 2022 Marvin Borner # Lists in Church/Boehm-Berarducci encoding using pairs # implementations are generally lazy (except when they're broken) -# TODO: Replace fold/map/etc. with faster LC native logic :import std/Combinator . :import std/Pair P @@ -85,6 +84,9 @@ eval-r z [[rec]] :test (~!(inc : (inc : {}(+1)))) ((+3)) +# returns the element at unary index in list +index-unary [[P.fst (0 P.snd 1)]] ⧗ (List a) → Unary → a + # returns the element at index in list index z [[[rec]]] ⧗ (List a) → Number → a rec 0 [[[case-index]]] case-end diff --git a/std/Math.bruijn b/std/Math.bruijn index 07a9a9b..1737572 100644 --- a/std/Math.bruijn +++ b/std/Math.bruijn @@ -1,4 +1,5 @@ # MIT License, Copyright (c) 2022 Marvin Borner +# experimental functions, sometimes list-based :input std/Number diff --git a/std/Number.bruijn b/std/Number.bruijn index ffc2591..f74b7d4 100644 --- a/std/Number.bruijn +++ b/std/Number.bruijn @@ -1,6 +1,6 @@ # MIT License, Copyright (c) 2023 Marvin Borner # this is just a reference to the ternary implementation -# read the readme for the reasoning of using balanced ternary by default +# read the wiki for the reasoning of using balanced ternary by default :import std/List . diff --git a/std/Number/Binary.bruijn b/std/Number/Binary.bruijn index ea837e3..28a3f7f 100644 --- a/std/Number/Binary.bruijn +++ b/std/Number/Binary.bruijn @@ -1,4 +1,5 @@ # MIT License, Copyright (c) 2023 Marvin Borner +# binary implementation of T.Æ. Mogensen (see refs in README) # TODO: Use abstract representation for logic instead of listifying :import std/Combinator . diff --git a/std/Number/Ternary.bruijn b/std/Number/Ternary.bruijn index e9b402c..e1b3893 100644 --- a/std/Number/Ternary.bruijn +++ b/std/Number/Ternary.bruijn @@ -1,7 +1,6 @@ # MIT License, Copyright (c) 2022 Marvin Borner -# This file defines the most basic mathematical operations +# ternary implementation of T.Æ. Mogensen and Douglas W. Jones (see refs in README) # → refer to std/Math for more advanced functions -# Heavily inspired by the works of T.Æ. Mogensen and Douglas W. Jones (see refs in README) :import std/Box B :import std/Combinator . diff --git a/std/Tree/Rose.bruijn b/std/Tree/Rose.bruijn index 90abeec..1b1e319 100644 --- a/std/Tree/Rose.bruijn +++ b/std/Tree/Rose.bruijn @@ -34,7 +34,7 @@ empty? [L.empty? ~0] ⧗ (RoseTree a) → Boolean ∅?‣ empty? -:test (∅?({ 'a' : (({:}'b') : L.empty) })) (false) +:test (∅?({ 'a' : ({:}'b' : L.empty) })) (false) :test (∅?({:}'a')) (true) # applies a function to leaf and the leafs of all branches @@ -43,7 +43,7 @@ map z [[[rec]]] ⧗ (a → b) → (RoseTree a) → (RoseTree b) …<$>… map -:test (map ^‣ ({ "woo" : ({:}"oof" : (({ "aah" : (({:}"huh" : L.empty)) }) : L.empty)) })) ({ 'w' : ({:}'o' : (({ 'a' : ({:}'h' : L.empty) }) : L.empty)) }) +:test (map ^‣ ({ "woo" : ({:}"oof" : (({ "aah" : ({:}"huh" : L.empty) }) : L.empty)) })) ({ 'w' : ({:}'o' : (({ 'a' : ({:}'h' : L.empty) }) : L.empty)) }) # maps a function returning list of trees and concatenates concat-map L.concat ∘∘ map ⧗ ((RoseTree a) → (List (RoseTree b))) → (List (RoseTree a)) → (List (RoseTree b))