[Перевод] Лямбда-исчисление в 397 байтах
Лямбда-исчисление — это язык программирования с единственным ключевым словом. Это асфальтовая топь Тьюринга, обнаруженная научным руководителем Тьюринга. В этом посте я расскажу о совершенно новой 397-байтной реализации двоичного лямбда-исчисления в виде Linux ELF для x86–64. Также в нём представлены удобно портируемый код на C и собранные двоичные файлы APE для других платформ.
SectorLambda реализует виртуальную машину Чёрча-Кривина-Тромпа с монадным вводом-выводом. В 397 байтах нам удалось реализовать сборку мусора, «ленивые» списки и хвостовую рекурсию. Интерпретатор извлекает самый младший бит из каждого байта stdin. Вывод состоит из байтов 0 и 1. Он 64-битный, однако смещение ограничено [0,255], поэтому программы не могут быть слишком большими. Поэтому это интересный инструмент для обучения, однако имеется 520-байтная версия для приложений более промышленного масштаба, обходящая многие подобные ограничения; впрочем, в ней нужно писать код ещё большей сложности.
-rwxr-xr-x 1 jart jart 397 Feb 27 12:15 blc-rw-r--r-- 1 jart jart 17K Feb 27 12:15 blc.S
Виртуальную машину можно скомпилировать в Linux для Linux x64 следующим образом:
cc -c -o blc.o blc.Sld.bfd -o blc blc.o -T flat.lds
Программа считывается из stdin, за которым следует его ввод. Вот простой туториал по использованию функции тождественности (λ 0), в двоичном лямбда-исчислении кодируемой как (00 10):
$ { printf 0010; printf 0101; } | ./blc; echo
0101
Если вы пользуетесь Mac, Windows, FreeBSD, NetBSD или OpenBSD, то можете вместо этого сделать следующее:
$ curl https://justine.lol/lambda/lambda.com >lambda.com
$ chmod +x lambda.com
$ { printf 0010; printf 0101; } | ./lambda.com; echo
0101Почему это важно
Программы, написанные на двоичном лямбда-исчислении, невероятно малы. Например, метациклический интерпретатор занимает всего 232 бита. Если работать с 8-битной версией интерпретатора (Blc с заглавной буквы), использующей истинный binary wire format, то мы можем получить представление о том, насколько малы могут быть программы, целевой платформой которых является виртуальная машина.
$ curl https://justine.lol/lambda/uni.Blc >uni.Blc
$ curl https://justine.lol/lambda/Blc >Blc
$ chmod +x Blc
$ { cat uni.Blc; printf ' '; printf 'hello world'; } | ./Blc; echo
hello world
$ ls -hal uni.Blc
-rw-r--r-- 1 jart jart 43 Feb 17 21:24 uni.Blc
Это означает, что наша 521-байтная виртуальная машина достаточно выразительна, чтобы реализовать себя всего в 43 байтах, то есть в меньше чем одной десятой от своего размера! Также в качестве виртуальной машины она имеет возможности, которых не хватает JVM, хотя и меньше неё на шесть порядков величин. Что-то подобное может иметь практическое применение в форматах сжатия, которым нужен маленький busy beaver, способный создавать большие объёмы данных. Кроме того, это просто круто.
Например, если вы собрали инструмент для сжатия, с его помощью можно закодировать файл как генерирующее его лямбда-выражение. Так как сложно внедрять новый формат сжатия, который не установлен у большинства людей, можно создать префикс сжатого файла с этим 397-байтным интерпретатором, получив автономный самораспаковывающийся архив, которым может пользоваться каждый. Кроме того, двоичное лямбда-исчисление будет более логичным в качестве встроенного микропроцессора, чем LISP.
Компиляция
Программы кодируются в следующем формате:
00 means abstraction (pops in the Krivine machine) 01 means application (push argument continuations) 1...0 means variable (with varint de Bruijn index)
Можно использовать шелл-скрипты sed в качестве компилятора байт-кода. Ему достаточно делать s/λ/00/g, s/\[/01/g, s/[^01]//g и т. д.
#!/bin/sh
tr \\n n |
sed '
s/;.*//
s/#.*//
s/1/⊤/g
s/0/⊥/g
s/λ/00/g
s/\[/01/g
s/9/11111111110/g
s/8/1111111110/g
s/7/111111110/g
s/6/11111110/g
s/5/1111110/g
s/4/111110/g
s/3/11110/g
s/2/1110/g
s/⊤/110/g
s/⊥/10/g
s/[^01]//g
'
Теперь мы можем писать более красивые программы:
{ printf %s "(λ 0)" | ./compile.sh
printf 00010101
} | ./blc
Программирование
Эта программа означает exit(0), потому что она возвращает $nil или []:
λ λλ0
Эта программа возвращает [⊥,⊤] поэтому выводит 10.
λ [[$pair $false] [[$pair $true] $nil]]
Эта программа означает if (1 - 1 == 0) putc('1') else putc('0'):
λ [[[$if [$iszero [[$sub $one] $one]]]
[[$pair $false] $nil]]
[[$pair $true] $nil]]
Эта программа делает то же самое, что и программа ident, но написана более обстоятельно. Среда выполнения передаёт два аргумента, gro и put (или λ [[0 wr0] wr1]). Индекс 110 — это внешний параметр, а 10 — внутренний. То есть эта программа эквивалентна for (;;) putc(getc())
λλ [1 0] ││ │└binds `put` or `(λ 0 wr0 wr1)` [cited as 0] └binds `gro` or `⋯` [cited as 1]
Эта программа инвертирует поток битов при помощи Y-комбинатора. Её скорость обработки составляет аж целых 16 кБ/с.
# a.k.a. Y(λfi.i(λbjn.❬¬b,fj❭)⊥)
[$Y λλ [[[$if 0] λλλ [[$pair [$not 2]] [4 1]]] $nil]]
││ │││
││ ││└consumes $nil terminator [uncited]
││ │└binds
