diff options
| -rw-r--r-- | docs/index.html | 4 | ||||
| -rw-r--r-- | docs/script.js | 8 | ||||
| -rw-r--r-- | docs/wiki_src/coding/meta-programming.md | 4 | ||||
| -rw-r--r-- | docs/wiki_src/introduction/lambda-calculus.md | 32 | ||||
| -rw-r--r-- | docs/wiki_src/introduction/syntax.md | 4 | ||||
| -rw-r--r-- | readme.md | 2 | ||||
| -rw-r--r-- | src/Helper.hs | 2 | ||||
| -rw-r--r-- | std/Number/Bruijn.bruijn | 6 |
8 files changed, 31 insertions, 31 deletions
diff --git a/docs/index.html b/docs/index.html index d5edad4..837492f 100644 --- a/docs/index.html +++ b/docs/index.html @@ -5,7 +5,7 @@ <meta name="viewport" content="width=device-width" /> <meta name="description" - content="Functional programming language based on pure De Bruijn indexed lambda calculus." + content="Functional programming language based on pure de Bruijn indexed lambda calculus." /> <link rel="stylesheet" href="style.css" type="text/css" media="all" /> <title>bruijn programming language</title> @@ -28,7 +28,7 @@ <div class="right"> <p> - Functional programming language based on pure De Bruijn indexed lambda + Functional programming language based on pure de Bruijn indexed lambda calculus. </p> </div> diff --git a/docs/script.js b/docs/script.js index 463badd..b388472 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 De 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. 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", "This number references the nth abstraction, starting counting from the inside. These 'De 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("meta", "This is the quote operator. It converts any given expression to bruijn's meta encoding. The meta encoding can be used for self modification and can be turned back to normal bruijn code."); @@ -46,8 +46,8 @@ 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 De 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."); -describe("unary", "Syntactic sugar for a unary number representation using abstractions as data. This is commonly known as a Church numeral. Needs a sign and brackets to differentiate it from De Bruijn indices."); +describe("unary", "Syntactic sugar for a unary number representation using abstractions as data. This is commonly known as a Church numeral. Needs a sign and brackets to differentiate it from de Bruijn indices."); document.body.addEventListener("click", clearPopups, true) diff --git a/docs/wiki_src/coding/meta-programming.md b/docs/wiki_src/coding/meta-programming.md index a77ecbe..c3577ca 100644 --- a/docs/wiki_src/coding/meta-programming.md +++ b/docs/wiki_src/coding/meta-programming.md @@ -37,7 +37,7 @@ again. :test (`[0 `,[0]]) (`[0 [0]]) ``` -Unquoted De Bruijn indices will get bound to the respective abstraction +Unquoted de Bruijn indices will get bound to the respective abstraction outside of its meta encoding. ``` bruijn @@ -46,7 +46,7 @@ add-two `[0 + (+2u)] :test (!add-two (+2u)) ((+4u)) -# adds two using a reaching De Bruijn index +# adds two using a reaching de Bruijn index add-two* [`(,0 + (+2u))] :test (!(add-two* `(+2u))) ((+4u)) diff --git a/docs/wiki_src/introduction/lambda-calculus.md b/docs/wiki_src/introduction/lambda-calculus.md index 067eaad..0d6af8e 100644 --- a/docs/wiki_src/introduction/lambda-calculus.md +++ b/docs/wiki_src/introduction/lambda-calculus.md @@ -1,6 +1,6 @@ # Lambda calculus -Bruijn is based on De Bruijn indexed lambda calculus. +Bruijn is based on de Bruijn indexed lambda calculus. ## Traditional lambda calculus @@ -11,15 +11,15 @@ Lambda calculus basically has three types of terms: `E` respectively. It's helpful to think of abstractions as anonymous functions. - *Application*: `(f x)` applies `f` to `x` -- the standard convention - allows repeated left-associative application: `(f x y z)` is + allows repeated left-associative application: `f x y z` is `(((f x) y) z)`. Combining these terms and removing redundant parentheses can result in -terms like λx.λy.x y, basically representing a function with two +terms like `λx.λy.x y`, basically representing a function with two parameters that uses its second parameter as an argument for its first. Evaluating terms is called *reduction*. There's only one rule you need -to know: `((λx.E) A)` becomes `E[x := A]` -- that is, calling an +to know: `(λx.E A)` becomes `E[x := A]` -- that is, calling an abstraction with an argument substitutes the argument inside the body of the abstraction ("β-reduction"). There are many different kinds of reduction techniques, but they basically all come back to this simple @@ -28,11 +28,11 @@ the order of reduction doesn't change the eventual result. When we talk about reduction in bruijn, we typically mean "reduction until normal form" -- we reduce until the term can't be reduced any -further (there does not exist any `((λx.E) A)`). +further (there does not exist any `(λx.E A)`). - ((λx.x) (λx.x)) ⤳ (λx.x) - ((λx.x) (λx.λy.x)) ⤳ (λx.λy.x) - ((λx.λy.x) (λx.x)) ⤳ (λy.λx.x) + (λx.x λx.x) ⤳ λx.x + (λx.x λx.λy.x) ⤳ λx.λy.x + (λx.λy.x (λx.x) ⤳ λy.λx.x ## De Bruijn indices @@ -43,15 +43,15 @@ many variables it's also really complicated to compare two expressions, since you first need to resolve shadowed and conflicting variables ("α-conversion"). -De Bruijn replace the concept of variables by using numeric references -to the abstraction layer. Let me explain using an example: The -expression `λx.x` becomes `λ0` -- the `0` refers to the first parameter -of the abstraction. Subsequently, the expression `λx.λy.x y` becomes -`λλ1 0`. Basically, if you're reading from left to right starting at the -abstraction you want to bind, you increment on every occurring `λ` until -you arrive at the index. +De Bruijn indices replace the concept of variables by using numeric +references to the abstraction layer. Let me explain using an example: +The expression `λx.x` becomes `λ0` -- the `0` refers to the first +parameter of the abstraction. Subsequently, the expression `λx.λy.x y` +becomes `λλ1 0`. Basically, if you're reading from left to right +starting at the abstraction you want to bind, you increment on every +occurring `λ` until you arrive at the index. -While confusing at first, programs written with De Bruijn indices can +While confusing at first, programs written with de Bruijn indices can actually be way easier to understand than the equivalent program with named variables. diff --git a/docs/wiki_src/introduction/syntax.md b/docs/wiki_src/introduction/syntax.md index e14f8c6..7a3256d 100644 --- a/docs/wiki_src/introduction/syntax.md +++ b/docs/wiki_src/introduction/syntax.md @@ -2,7 +2,7 @@ Bruijn has an arguably weird syntax, although it's not strictly meant as an esoteric programming language. Most notably the usage of lambda -calculus logic, combinators, and De Bruijn indices can be confusing at +calculus logic, combinators, and de Bruijn indices can be confusing at first -- it's definitely possible to get used to them though! Bruijn uses a [variation of lambda calculus](lambda-calculus.md). For @@ -42,7 +42,7 @@ normal lambda calculus reducer. ## Open terms -If you use De Bruijn indices that reach out of their environment, you +If you use de Bruijn indices that reach out of their environment, you have created an *open term*. Depending on the context, these terms are typically seen as invalid if standing by themself. @@ -3,7 +3,7 @@ </p> > A purely functional programming language based on lambda calculus and -> De Bruijn indices written in Haskell. +> de Bruijn indices written in Haskell. Pronunciation: `/bɹaʊn/`. diff --git a/src/Helper.hs b/src/Helper.hs index edd9b09..695d63f 100644 --- a/src/Helper.hs +++ b/src/Helper.hs @@ -407,7 +407,7 @@ decimalToUnary n | n < 0 = decimalToUnary 0 gen 0 = Bruijn 0 gen n' = Application (Bruijn 1) (gen (n' - 1)) --- Decimal to De Bruijn encoding +-- Decimal to de Bruijn encoding decimalToDeBruijn :: Integer -> Expression decimalToDeBruijn n | n < 0 = decimalToDeBruijn 0 | otherwise = gen n diff --git a/std/Number/Bruijn.bruijn b/std/Number/Bruijn.bruijn index 131a1a3..585d3bc 100644 --- a/std/Number/Bruijn.bruijn +++ b/std/Number/Bruijn.bruijn @@ -1,10 +1,10 @@ # MIT License, Copyright (c) 2023 Marvin Borner -# De Bruijn numeral system (named by me) +# de Bruijn numeral system (named by me) # proof that this numeral system does not support zero/eq/sub/etc. is in # Wadsworth, Christopher. "Some unusual λ-calculus numeral systems." # very sad indeed -# increments De Bruijn numeral +# increments de Bruijn numeral inc [[[2 1]]] ++‣ inc @@ -12,7 +12,7 @@ inc [[[2 1]]] :test (++(+0d)) ((+1d)) :test (++(+5d)) ((+6d)) -# decrements De Bruijn numeral +# decrements de Bruijn numeral dec [[1 0 0]] --‣ dec |