From bfc12aff90252dbcd9c40a1d095052ed771d4e56 Mon Sep 17 00:00:00 2001 From: Marvin Borner Date: Fri, 17 Jun 2022 18:10:45 +0200 Subject: Documentation --- LICENSE | 30 ------------ README.md | 159 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++- 2 files changed, 158 insertions(+), 31 deletions(-) delete mode 100644 LICENSE diff --git a/LICENSE b/LICENSE deleted file mode 100644 index 342c588..0000000 --- a/LICENSE +++ /dev/null @@ -1,30 +0,0 @@ -Copyright Author name here (c) 2022 - -All rights reserved. - -Redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - - * Redistributions of source code must retain the above copyright - notice, this list of conditions and the following disclaimer. - - * Redistributions in binary form must reproduce the above - copyright notice, this list of conditions and the following - disclaimer in the documentation and/or other materials provided - with the distribution. - - * Neither the name of Author name here nor the names of other - contributors may be used to endorse or promote products derived - from this software without specific prior written permission. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS -"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT -LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR -A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT -OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, -SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT -LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, -DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY -THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT -(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/README.md b/README.md index c443c77..9d68478 100644 --- a/README.md +++ b/README.md @@ -1 +1,158 @@ -# bruijn +# Bruijn + +A purely academic programming language based on lambda calculus and De +Bruijn indices written in Haskell. + +## Features + +- De Bruijn indices\[0\] eliminate the complexity of α-equivalence and + α-conversion +- Unique bracket-style representation for lambda abstractions enables + improved human-readability and faster syntactic perception +- Balanced ternary allows negative numbers while having a reasonably + compact representation, operator and time complexity (in comparison + to unary/binary church numerals)\[1\] +- Highly space-efficient compilation to binary lambda calculus + (BLC)\[2\]\[3\] additionally to normal interpretation and REPL +- Recursion can be implemented using combinators such as Y or ω +- Included standard library featuring many useful functions + (`std.bruijn`) + +## Basics + +### De Bruijn indices + +De Bruijn indices\[0\] replace the concept of variables in lambda +calculus. The index basically represents the abstraction layer you want +to reference beginning at 0 with the innermost layer. + +For example, λx.x becomes λ0 because x referenced the first abstraction +layer. Furthermore, λx.λy.xy becomes λλ10 and so forth. + +You can read more about De Bruijn indices on +[Wikipedia](https://en.wikipedia.org/wiki/De_Bruijn_index). + +### Syntax + +In general the syntax is pretty similar to the previously presented +normal lambda calculus syntax with De Bruijn indices. + +You can use any function that you’ve previously defined. You can also +overwrite previously defined functions. The environment gets interpreted +from down to top. + +The following are the main syntax specifications in the (minorly +extended) [Backus-Naur +form](https://en.wikipedia.org/wiki/Backus%E2%80%93Naur_form). Spaces +are optional but allowed. + + ::= [a-ω,A-Ω,_][a-ω,A-Ω,0-9,?,!,',_]* + ::= "[" "]" + ::= ("+" | "-")[0-9]+ + ::= [0-9] + ::= | | | "(" ")" | + ::= + ::= | + ::= ":test " = + ::= ":import " + ::= "# " * + +The following are the differences in syntax between REPL and file: + +**For files**: + +The execution of a file begins at the `main` function. Its existence is +mandatory. + + ::= ":print " + ::= + ::= | | | | | "\n" + +**For REPL**: + + ::= = + ::= | | | | | "\n" + +### Standard library + +You may want to use the included standard library to reach your +program’s full potential. It includes many common combinators as well as +functions for numerical, boolean and IO operations and much more. + +You can import it from `std.bruijn` using `:import std`. + +### Examples + +Plain execution + + # equivalent of λx.x + id [0] + + # equivalent of (λx.x) (λx.λy.x) = λx.λy.x + :test id [[1]] = [[1]] + + # endless loop using omega combinator + om [0 0] + nom om + main om nom + +Using standard library + + :import std + + # equivalent of (λx.x) (λx.λy.x) = λx.λy.x + outer id [[1]] + :test outer = [[1]] + + # pairs + me [[[1]]] + you [[[2]]] + love pair me you + :test fst love = me + :test snd love = you + + # boolean + main not (or (and false true) true) + :test main = [0] + +### Compilation to BLC + +You can compile bruijn to John Tromp’s BLC\[2\]\[3\]. Only the used +functions actually get compiled in order to achieve a minimal binary +size. + +BLC uses the following encoding: + +| term | lambda | bruijn | BLC | +|:-------------|:-------|:-------|:-----------------| +| abstraction | λM | \[M\] | 00M | +| application | MN | MN | 01MN | +| bruijn index | i | i | 1i+10 | + +## Installation + +You first need to install Haskell and Haskell Stack using the guidelines +of your operating system. + +Using Haskell Stack, run `stack run -- [args]` to play around and use +`stack install` to install bruijn into your path. + +## Usage + +Please read the usage information in the executable by using the `-h` +argument. + +## 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\] Tromp, John. “Binary lambda calculus and combinatory logic.” + Randomness and Complexity, from Leibniz to Chaitin. 2007. 237-260. +- \[3\] Tromp, John. “Functional Bits: Lambda Calculus based + Algorithmic Information Theory.” (2022). -- cgit v1.2.3