I wrote this package to play around with the Binary Lambda Calculus (originally defined by John Tromp). During working on that, I separated out the representation of terms into the package LambdaCalculus.jl, which now is a dependency here.
The basic feature of the binary calculus is that it is just prefix-free encoding of terms in De Bruijn form:
julia> pair = LambdaCalculus.DeBruijn.@lambda f -> f(one, two)
(λ.((1 3) 2))
julia> encode(pair)
"\0\0\0\x01\0\x01\x01\0\x01\x01\x01\0\x01\x01\0"
julia> encode(pair) |> decode
(λ.((1 3) 2))
In addition to that, I reimplemented the counting and unranking functions from “Counting and Generating Terms in the Binary Lambda Calculus by Grygiel and Lescanne, which allow one, for example, to enumerate all lambda terms of a certain (binary) size:
julia> collect(terms(0, 10))
6-element Array{LambdaCalculus.DeBruijn.Term,1}:
(λ.(λ.(λ.(λ.1))))
(λ.(λ.(λ.3)))
(λ.(λ.(1 1)))
(λ.(1 (λ.1)))
(λ.((λ.1) 1))
((λ.1) (λ.1))
julia> grygiel_lescanne(0, 20)
883
julia> grygiel_lescanne(0, 20) == length(collect(terms(0, 20)))
true
(And terms is an iterator, of course.)
Pkg.add("git@github.com:phipsgabler/BinaryLambdaCalculus.jl.git")
This work is licensed under an MIT license.