#### um-abt

**Table of Contents**

### Overview

`um-abt`

is 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

general syntactic (perhaps later also equational) unification. We might

therefore describe this library as an implentation of*unifiable*abstract

binding trees (or UABTs). ABTs provide a generalized a reusable system for

variable binding for any language implemented in its terms. UABTs provide --

in addition -- a generalized, reusable system for (first-order, syntactic)

unification for any language implemented in*its*terms.Unification is lovely and not used nearly enough, imo.

It implements variable binding via (what we might call)

*binding by*; i.e., variable binding is implemented by way of "immutable"

reference

reference cells. I suspect the advantages of this approach to include:a trivial algorithm for computing ɑ-equivalence

neutralization of the usual problem of renaming bound variables

the representation is easy to read, in contrast with De Bruijn indices,

and, even more important, there's no tedious bookkeeping required during

substitution.the representation is trivial to inspect and manipulate, in contrast with

HOAS

Note that I have not done any rigorous analysis or other work to test these

suspicions. Feedback or correction on these points would be welcome.I also suspect this approach lacks the safety and formal elegance of HOAS or

NbE. The

approach used here is also dependent on OCaml's definition of physical

equality to identify`ref`

cells, and on MLs ability to ensure that the

references are immutable via type abstraction.

### 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 simply typed

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.

The generated ABT will have the following form, where `module O : Operator`

:

```
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:

```
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]
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 `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`

. We

use pattern matching to j

```
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 a the free variable "M" with the body of the [k] combinator *)
let unified_term = (lam "x" (v "M") =.= k) |> Result.get_ok in
assert (to_string unified_term = "(λx.(λy.x))");
(* 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 implementation that takes this connection literally to bypass the

usual pain of tedious renaming and inscrutable De Bruijn indices.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".The implementation of ABTs in OCaml was informed by Neel

Krishnaswami's post on

ABTs

(but is substantialy different).

sha256=454f85bde8c196e2ea7abd05a593155c3fea3de4c456d6142a56b161e8726b49

sha512=cbb2425262c392b760f270174fedbadc86af2a9af5cecf95ec02a7bcca36921dda163a0407f32b5ce6eb6843364a187698af8e642d5e2cfaf87ae3086f4b211d

with-doc

with-test & >= "1.10.1"

with-test & >= "0.2.0"

with-test & >= "0.17"

>= "0.2.0"

>= "0.7.0"

>= "5.2.1"

>= "v0.14.1"

>= "4.08.0"

>= "2.8"