package um-abt

Overview

um-abt is a library for constructing and manipulating the abstract syntax of languages that use variables.

um-abt provides unifiable abstract binding trees (UABTs). An abstract binding tree (ABT) is an abstract syntax tree (AST), enriched with constructs to manage variable binding and scope.

um-abt extends ABTs with support for nominal unification (unificaiton modulo ɑ-equivalence).

Example

A succinct example of the typical use of this library can be seen in the following implementation of the untyped λ-calculus.

Define your language's operators:

(* 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

(Note the use of ppx_deriving to derive most values automatically.)

Generate your the ABT representing your syntax, and define combinators to easily and safely construct terms of your lanugage construct:

(* Generate the syntax, which will include a type [t] of the ABTs over the operators **)
open 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))

Define the dynamics of your language (here using the variable substitution function subst, provided by the generated 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

Enjoy unification and ɑ-equivalence:

(* An example term *)
let k = lam "x" (lam "y" x)

(* 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);

(* 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))");

Modules and interfaces