blc
| Crates.io | blc |
| lib.rs | blc |
| version | 0.6.0 |
| source | src |
| created_at | 2017-04-07 13:11:23.547599 |
| updated_at | 2018-01-26 15:31:20.63939 |
| description | An implementation of the binary lambda calculus. |
| homepage | |
| repository | https://github.com/ljedrz/blc |
| max_upload_size | |
| id | 9927 |
| size | 36,010 |
(ljedrz)
documentation
README
blc
blc is an implementation of the binary lambda calculus.
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 (hex) | 16 16 c 2c 10 b0 42 c1 85 83 b 6 16 c 2c 10 41 0 |
Documentation
Status
The library is already usable, but it is still a work in progress.
TODO
- better documentation
- more blc examples