From b867e4ab6fe5bd8b372e33aa4d1b063908149754 Mon Sep 17 00:00:00 2001 From: opfez Date: Sun, 1 Aug 2021 21:46:06 +0200 Subject: [PATCH] [lambda-calculus.wtn] add note about de brujin indexing --- format.c | 2 +- site-src/lambda-calculus.wtn | 5 +++++ 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/format.c b/format.c index ae87a91..9f827e7 100644 --- a/format.c +++ b/format.c @@ -288,7 +288,7 @@ main(int argc, char *argv[]) char bn[80] = {0}; basename(argv[1], bn, '.'); - char out_name[80] = {0}; + char out_name[85] = {0}; sprintf(out_name, "%s.html", bn); out = fopen(out_name, "w"); diff --git a/site-src/lambda-calculus.wtn b/site-src/lambda-calculus.wtn index e54814d..a388a00 100644 --- a/site-src/lambda-calculus.wtn +++ b/site-src/lambda-calculus.wtn @@ -21,6 +21,11 @@ expression following the period. λx.x is therefore the function that takes one argument and evaluates to that argument. An example of applying this function is (λx.x) y → y. +Using De Brujin indexing, variable names are no longer necessary. With this +indexing system, each variable name instance is replaced by an index. The +K-combinator (λx.λy.x) is expressed with De Brujin indexing as λ λ 2. The '2' is +the index, which refers to the variable bound by the lambda form 2 levels. + ** Reduction There are two ways of reducing an expression, α-conversion and