Initial commit

3 files changed, 195 insertions, 0 deletions

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..bba61c4
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,6 @@
+build/
+.cache/
+
+*.plist
+tags
+compile_commands.json
diff --git a/makefile b/makefile
new file mode 100644
index 0000000..1058de6
--- /dev/null
+++ b/makefile
@@ -0,0 +1,50 @@
+# Copyright (c) 2024, Marvin Borner <dev@marvinborner.de>
+# SPDX-License-Identifier: MIT
+
+CC = gcc
+TG = ctags
+
+BUILD = ${CURDIR}/build
+SRC = ${CURDIR}/src
+INC = ${CURDIR}/inc
+SRCS = $(wildcard $(SRC)/*.c)
+OBJS = $(patsubst $(SRC)/%.c, $(BUILD)/%.o, $(SRCS))
+
+CFLAGS_DEBUG = -fsanitize=address,leak,undefined -g -O0
+CFLAGS_WARNINGS = -Wall -Wextra -Wshadow -Wpointer-arith -Wwrite-strings -Wredundant-decls -Wnested-externs -Wmissing-declarations -Wstrict-prototypes -Wmissing-prototypes -Wcast-qual -Wswitch-default -Wswitch-enum -Wunreachable-code -Wundef -Wold-style-definition -pedantic -Wno-switch-enum
+CFLAGS = $(CFLAGS_WARNINGS) -std=c99 -Ofast -I$(INC)
+
+ifdef DEBUG # TODO: Somehow clean automagically
+CFLAGS += $(CFLAGS_DEBUG)
+endif
+
+ifeq ($(PREFIX),)
+    PREFIX := /usr/local
+endif
+
+all: compile
+
+full: all sync
+
+compile: $(BUILD) $(OBJS) $(BUILD)/bloc
+
+clean:
+	@rm -rf $(BUILD)/*
+
+install:
+	@install -m 755 $(BUILD)/bloc $(DESTDIR)$(PREFIX)/bin/
+
+sync: # Ugly hack
+	@$(MAKE) $(BUILD)/bloc --always-make --dry-run | grep -wE 'gcc|g\+\+' | grep -w '\-c' | jq -nR '[inputs|{directory:".", command:., file: match(" [^ ]+$$").string[1:]}]' >compile_commands.json
+	@$(TG) -R --exclude=.git --exclude=build .
+
+$(BUILD)/%.o: $(SRC)/%.c
+	@$(CC) -c -o $@ $(CFLAGS) $<
+
+$(BUILD)/bloc: $(OBJS)
+	@$(CC) -o $@ $(CFLAGS) $^
+
+.PHONY: all compile clean sync
+
+$(BUILD):
+	@mkdir -p $@
diff --git a/readme.md b/readme.md
new file mode 100644
index 0000000..6071510
--- /dev/null
+++ b/readme.md
@@ -0,0 +1,139 @@
+# BLC Experiments
+
+Small experiment to find the smallest binary encoding of lambda terms. I
+use an empirical approach with the terms located in `samples/`. The
+source also serves as a reference C implementation of BLC encodings.
+
+Of course, encodings that allow sharing of duplicate terms (e.g. in a
+binary encoded DAG) can yield even smaller encodings. I’ve done that in
+the [BLoC](https://github.com/marvinborner/BLoC) encoding and I will
+apply the insights from this experiments there as well.
+
+## Traditional BLC
+
+$$
+\begin{aligned}
+f(\lambda m)  &= 00\ f(M)\\
+f(M N)        &= 01\ f(M)\ f(N)\\
+f(i)          &= 1^i\ 0
+\end{aligned}
+$$
+
+**Problem**: de Bruijn indices are encoded in *unary* ($O(n)$).
+
+### Statistics
+
+TODO
+
+### Resources:
+
+- [Binary Lambda
+  Calculus](https://tromp.github.io/cl/Binary_lambda_calculus.html)
+  (John Tromp)
+
+## Levenshtein Indices (BLC2)
+
+$$
+\begin{aligned}
+f(\lambda M)  &= 00\ f(M)\\
+f(M N)        &= 01\ f(M)\ f(N)\\
+f(i)          &= \mathrm{code}(i)
+\end{aligned}
+$$
+
+### Statistics
+
+TODO (compare with blc)
+
+### Resources
+
+- [Levenshtein Coding](https://en.wikipedia.org/wiki/Levenshtein_coding)
+  (Wikipedia)
+
+## Mateusz Naściszewski
+
+$$
+\begin{aligned}
+f(t)            &= g(0, t)\\
+g(0, i)         &= \text{undefined}\\
+g(1, 0)         &= 1\\
+g(n, 0)         &= 10\\
+g(n, i)         &= 1\ g(n-1, i-1)\\
+g(0, \lambda M) &= 0\ g(1, M)\\
+g(n, \lambda M) &= 00\ g(n+1, M)\\
+g(0, M\ N)      &= 1\ g(1, M)\\
+g(n, M\ N)      &= 01\ g(n, M)\ g(n, N)
+\end{aligned}
+$$
+
+### Statistics
+
+TODO
+
+### Resources
+
+- [Implementation](https://github.com/tromp/AIT/commit/f8c7d191519bc8df4380d49934f2c9b9bdfeef19)
+  (John Tromp)
+
+## Merged Left-Apps
+
+Here I “merge” multiple left applications with a single prefix. This
+uses one bit more for binary applications. However, practical lambda
+terms often use many consecutive left applications!
+
+$$
+\begin{aligned}
+f(\lambda M)    &= 01\ f(M)\\
+f(M_1\dots M_n) &= 0^n\ 1\ f(M_1)\dots f(M_n)\\
+f(i)            &= 1^i 0
+\end{aligned}
+$$
+
+### Statistics
+
+TODO
+
+### Resources
+
+- None?
+
+## Merged Multi-Abs
+
+Here I “merge” multiple abstractions with a single prefix.
+
+$$
+\begin{aligned}
+f(\lambda_1\dots \lambda_n M) &= 0^{n+1}\ 1\ f(M)\\
+f(M\ N)                       &= 01\ f(M)\ f(N)\\
+f(i)                          &= 1^i 0
+\end{aligned}
+$$
+
+Slightly better, I can combine this with the previous technique!
+
+$$
+\begin{aligned}
+f(\lambda_1\dots \lambda_n M) &= 0^n\ 11\ f(M)\\
+f(M_1\ M_n)                   &= 0^n\ 10\ f(M_1)\dots f(M_n)\\
+f(i)                          &= 1^i 0
+\end{aligned}
+$$
+
+Or, merge it directly! The *trick* is to see applications as zeroth
+abstractions. Any immediate applications inside abstractions are handled
+directly by the abstraction constructor.
+
+$$
+\begin{aligned}
+f(\lambda_1\dots \lambda_n (M_1\dots M_m)) &= 0^n\ 1\ 0^m\ 1\ f(M_1)\dots f(M_n)\\
+f(i)                                       &= 1^i 0
+\end{aligned}
+$$
+
+### Statistics
+
+TODO
+
+### Resources
+
+- None?