Crate blc [] [src]

blc is an implementation of the binary lambda calculus in Rust.

Binary lambda calculus basics

Binary lambda calculus (BLC) is a minimal, purely functional programming language based on a binary encoding of the untyped lambda calculus with De Bruijn indices.

Lambda terms have the following representation in BLC:

term lambda BLC
abstraction λM 00M
application MN 01MN
variable i 1i0

Since BLC programs are basically lambda calculus terms, they can be applied to other terms. In order to be applicable to binary (but not BLC-encoded) input, it has to be lambda-encoded first. Bytestrings are lambda-encoded as Church lists of bytes and bytes are lambda-encoded as Church lists of lambda-encoded bits.

Bits 0 and 1 are lambda-encoded as Church booleans:

bit lambda BLC
0 λλ2 (true) 0000110
1 λλ1 (false) 000010

Example: BLC-encoding steps for a byte representing the ASCII/UTF-8 encoded letter 'a':

encoding representation
decimal 96
binary 01100001
lambda λ1(λλ2)(λ1(λλ1)(λ1(λλ1)(λ1(λλ2)(λ1(λλ2)(λ1(λλ2)(λ1(λλ2)(λ1(λλ1)(λλ1))))))))
BLC 00010110000101100000110000101100000100001011000001000010110000011000010110000011000010110000011000010110000011000010110000010000010000010



Binary encoding for lambda expressions


Binary lambda calculus execution


Lambda encoding for byte strings