#### um-abt

**Table of Contents**

### Overview

`um-abt`

is an OCaml library implementing abstract binding trees (ABTs)

exhibiting the properties defined in Robert

Harper's Practical Foundations for

Programming Labguages (PFPL).

#### Documentation

#### Aims

This library aims for the following qualities:

It should be correct.

It should be well tested, to ensure its correctness.

It should be easy to use.

It should be well documented.

#### Features

This ABT library has two distinctive (afaik) features:

The library augments the binding functionality of the ABT approach with

**unification modulo ɑ-equivalence**. We might therefore describe this

library as an implementation of*unifiable*abstract binding trees (or

UABTs): where ABTs provide a general and reusable system for variable

binding, UABTs add a general and reusable system for nominal unification.Unification is lovely and not used nearly enough, imo.

The library implements variable binding via (what we might call)

**binding by**; i.e., variable binding is recorded in the pointer structure of

reference

by way of "immutable" reference cells. This is somewhat of an experiment:

being unaware of other implementations using this approach, I worked out the

details as I went. So far, it seems to have yielded [trivial ɑ-equivalence

and substitution algorithms, and enabled nominal unification][], without

requiring any bureaucratic fiddling with renaming, variable permutations, or

fresh variables.

**Caveat emptor**: I am not an academic PLT researcher and this library has not

yet been used extensively.

#### Installation

The latest released version can be installed with

opam:

```
opam install um-abt
```

To install the head of development

```
opam pin git@github.com:shonfeder/um-abt.git
```

### Synopsis

The following short examples help illustrate use of the library. For more

extensive examples, see

test/example/example.ml.

#### An ABT for the λ-calculus

Here is a short example showing a naive implementation of the untyped lambda

calculus using `um-abt`

.

ABTs representing the syntax of a language are produced by applying the`Abt.Make`

functor to a module implementing the `Operator`

specification.

```
module Syntax = struct
(* Define the usual operators, but without the variables, since we get those free *)
module O = struct
type 'a t =
| App of 'a * 'a
| Lam of 'a
[@@deriving eq, map, fold, sexp]
let to_string : string t -> string = function
| App (l, m) -> Printf.sprintf "(%s %s)" l m
| Lam abs -> Printf.sprintf "(λ%s)" abs
end
(* Generate the syntax, which will include a type [t] of the ABTs over the operators **)
include Abt.Make (O)
(* Define some constructors to ensure correct construction *)
let app m n : t =
(* [op] lifts an operator into an ABT *)
op (App (m, n))
let lam x m : t =
(* ["x" #. scope] binds all free variables named "x" in the [scope] *)
op (Lam (x #. m))
end
```

The generated ABT will have the following form:

```
type t = private
| Var of Abt.Var.t
| Bnd of Abt.Var.binding * t
| Opr of t O.t
```

Most of the values required by the `Operator`

specification can be derived using`ppx_deriving`

. So all that is

usually required is to define a datatype representing the operators and their

arities.

After the ABT is generated However, it is recommended that one also define constructors making it

more convenient and safer to construct terms of the language.

The `private`

annotation indicates that you can use pattern matching to

deconstruct the ABT, but you cannot construct new values without using the

supplied combinators. This ensures essential invariants are preserved. E.g., it

is impossible to construct a binding in which the expected variables are not

bound in the term in scope.

For a more perspicuous view of our produce, let's define the SKI

combinators and see what

they look like when printed in the usual notation:

```
(* [v x] is a free variable named "x" *)
let x, y, z = Syntax.(v "x", v "y", v "z")
let s = Syntax.(lam "x" (lam "y" (lam "z" (app (app x y) (app y z)))))
let k = Syntax.(lam "x" (lam "y" x))
let i = Syntax.(lam "x" x)
let () =
assert (Syntax.to_string s = "(λx.(λy.(λz.((x y) (y z)))))");
assert (Syntax.to_string k = "(λx.(λy.x))");
assert (Syntax.to_string i = "(λx.x)");
```

Note that equality between ABTs is defined in terms of ɑ-equivalence, so we can

define the `i`

using any variable, and it will be equivalent:

```
let () =
assert Syntax.(equal i (lam "y" y))
```

Now let's define reduction, using the API provided by our generated `Syntax`

.`Syntax`

modules expose `private`

value constructors, which provide a

pattern-matching based interface for destructuring ABTs, but prevents

constructing new ABTs directly. This gives us the convenience of a pattern

matching API without compromising the integrity of the ABT representation by

allowing ill-formed structures.

```
open Syntax
let rec eval : t -> t =
fun t ->
match t with
| Opr (App (m, n)) -> apply (eval m) (eval n)
(* No other terms can be evaluated *)
| _ -> t
and apply : t -> t -> t =
fun m n ->
match m with
| Bnd (bnd, t) -> subst bnd ~value:n t
| Opr (Lam bnd) -> eval (apply bnd n)
(* otherwise the application can't be evaluated *)
| _ -> app m n
```

Finally, let's illustrate the correctness of our implementation with a few

simple evaluations, demonstrating that our SKI combinators behave as expected:

```
let () =
(* Let equality be ɑ-equivalence on our syntax for the following examples *)
let (=) = Syntax.equal in
let open Syntax in
assert (eval (app i x) = x);
assert (eval (app (app k x) y) = x);
assert (eval (app (app (app s x) y) z) = (app (app x y) (app y z)))
```

(See

https://en.wikipedia.org/wiki/SKI_combinator_calculus#Informal_description for

reference.)

#### Unification over λ-calculus terms

The ABTs produced by applying the `Abt.Make`

functor to an `Operator`

implementation support first-order, syntactic unification modulo ɑ-equivalence.

Unification is (currently) limited to first-order, because there is no support

for variables standing for operators.Unification is (currently) syntactic, because we do not perform any evaluation

to determine if two ABTs can be unified.Unification is modulo ɑ-equivalence, because two ɑ-equivalent ABTs are

considered equal during unification.

```
let () =
let open Syntax in
(* The generated [Syntax] module includes a [Unification] submodule
- the [=?=] operator checks for unifiability
- the [=.=] operator gives an [Ok] result with the unified term, if its operands unify,
or else an [Error] indicating why the unification failed
- the [unify] function is like [=.=], but it also gives the substitution used to produce
a unified term *)
let ((=?=), (=.=), unify) = Unification.((=?=), (=.=), unify) in
(* A free variable will unify with anything *)
assert (v "X" =?= s);
(* Again, unification is modulo ɑ-equivalence *)
assert (lam "y" (lam "x" y) =?= lam "x" (lam "y" x));
(* Here we unify the free variable "M" with the body of the [k] combinator,
note that the nominal unification is modulo bound variables: *)
let unified_term = (lam "z" (v "M") =.= k) |> Result.get_ok in
assert (to_string unified_term = "(λz.(λy.z))");
(* The substitution allows retrieval the bound values of the free variables *)
let _, substitution = unify (lam "x" (v "M")) k |> Result.get_ok in
assert (Unification.Subst.to_string substitution = "[ M -> (λy.x) ]")
```

### Additional References

Harper explicitly connects binding scope with pointers in PFPL (tho I have not

seen another functional implementation that takes this connection literally):I discussed the idea of using

`ref`

cells to track binding scope in

conversation with Callan McGill, and the representation of free and bound

variables was influenced by his post "Locally

Nameless".My initial implementation of an ABT library was informed by Neel

Krishnaswami's post on

ABTs.

There are still some aspects of that approach that show up here.I consulted Christian Urban's paper

Nominal Unification Revisited and

Urban, Pitts, and Gabby's Nominal

Unification for guidance on the

harrier bits of unification modulo ɑ-equivalence, tho this library does not

currently take advantage of the strategy of nominal permutations described

there.

sha256=9472873b4f485ff1c169d950488133c79efb4b00b757526bfb14a2f043a0480f

sha512=e3ea3990177778ae109082bea0b952b760b4fc9a243f0321367d2927061e3766c0d99679c5e4b13f89532b22ad4993c34f91b625ec40e07f113b9812521f91f4

with-doc

with-test & >= "1.10.1"

with-test & >= "0.2.0"

with-test & >= "0.17"

>= "0.2.0"

>= "v0.14.3"

>= "5.2.1"

>= "v0.14.1"

>= "v0.14.0"

>= "0.7.0"

>= "2.8"