🥮 mooncakes.io
README

#Terms

The HOL term language. Terms form a simply-typed lambda calculus with constants, represented using the locally nameless convention.

Depends on: foundation (for Subst), types (for Type, TypeSubst)

#The Term Enum

///|
enum Term {
  FVar(String, Type) // free (named) variable with its type
  BVar(Int) // bound variable (de Bruijn index)
  Const(String, Type) // declared constant (e.g., "=")
  App(Term, Term) // function application
  Abs(Term, Term) // lambda abstraction
}

#Why Locally Nameless?

Bound variables use de Bruijn indices (BVar(0) = innermost binder), while free variables use names (FVar("x", ty)). This means alpha-equivalent terms have identical representations:

// \x. x  and  \y. y  both become  Abs(_, BVar(0))

No alpha-conversion is needed during comparison -- structural equality suffices.

#Constant Table

The global signature of constants is stored in a mutable table. The only primitive constant is polymorphic equality:

= : 'a -> 'a -> bool

All other connectives (==>, /\, forall, etc.) are defined on top of equality (see the logic package). New constants are registered via @terms.Term::new_const (which also returns the new constant term) or Kernel::defineConst.

#Building Terms

///|
test "terms: free variables and constants" {
  @types.Type::reset_table()
  @terms.Term::reset_table()
  let bool_ty = @types.bool_ty()

  // Free variables carry a name and a type
  let p = @terms.mk_var("p", bool_ty)
  guard p is FVar(name, _) else { fail("expected FVar") }
  assert_eq(name, "p")

  // The primitive constant: = : 'a -> 'a -> bool
  let a = @types.mk_var("'a")
  let eq_ty = @types.mk_fun(a, @types.mk_fun(a, bool_ty))
  let eq_const = @terms.Term::mk_const("=", eq_ty)
  assert_true(eq_const is Const(_, _))
}

#Lambda Abstraction

mk_abs(x, body) replaces free occurrences of x in body with BVar(0), producing a locally nameless abstraction. dest_abs reverses the process, picking a fresh name to avoid capture:

///|
test "terms: abstraction roundtrip and type inference" {
  @types.Type::reset_table()
  @terms.Term::reset_table()
  let a = @types.mk_var("'a")
  let x = @terms.mk_var("x", a)

  // Build the identity: \x. x
  let id_fn = @terms.Term::mk_abs(x, x)
  assert_true(id_fn is Abs(_, _))
  assert_eq(@types.Type::pprint(id_fn.type_of()), "'a --> 'a")

  // Destruct it back
  let (bv, body) = id_fn.dest_abs()
  assert_eq(@terms.Term::pprint(body), @terms.Term::pprint(bv))
}

#Equations

mk_eq(l, r) builds the equation l = r, checking that both sides have the same type. Internally it instantiates the polymorphic = constant:

///|
test "terms: equations" {
  @types.Type::reset_table()
  @terms.Term::reset_table()
  let a = @types.mk_var("'a")
  let x = @terms.mk_var("x", a)
  let y = @terms.mk_var("y", a)

  let eq = @terms.Term::mk_eq(x, y)
  assert_true(@terms.Term::is_eq(eq))
  let (lhs, rhs) = @terms.Term::dest_eq(eq)
  assert_true(lhs == x)
  assert_true(rhs == y)
}

#Alpha-Convertibility

Because bound variables are de Bruijn indices, alpha-equivalent terms are structurally identical. aconv checks this:

///|
test "terms: alpha-convertibility" {
  @types.Type::reset_table()
  @terms.Term::reset_table()
  let a = @types.mk_var("'a")
  let x = @terms.mk_var("x", a)
  let y = @terms.mk_var("y", a)

  // \x. x  and  \y. y  are alpha-convertible
  assert_true(@terms.Term::mk_abs(x, x).aconv(@terms.Term::mk_abs(y, y)))
  // But x and y (as free variables) are NOT
  assert_false(x.aconv(y))
}

#Substitution

There are three kinds of substitution:

OperationWhat it does
tm.inst(sigma)Apply a type substitution to every type annotation in tm
tm.subst(sigma)Replace free term variables according to sigma
ty.subst(sigma)Replace type variables in a type (see types package)

Type instantiation is how polymorphic constants get specialized:

///|
test "terms: type instantiation" {
  @types.Type::reset_table()
  @terms.Term::reset_table()
  let a = @types.mk_var("'a")
  let bool_ty = @types.bool_ty()
  let eq_ty = @types.mk_fun(a, @types.mk_fun(a, bool_ty))
  let eq = @terms.Term::mk_const("=", eq_ty)

  // Instantiate 'a := bool
  let sigma : @types.TypeSubst = Subst(pairs=[(a, bool_ty)])
  let eq_bool = eq.inst(sigma)
  let expected = @types.mk_fun(bool_ty, @types.mk_fun(bool_ty, bool_ty))
  assert_true(eq_bool.type_of() == expected)
}

#Term Matching

pattern.match_term(observation) finds both a term substitution and a type substitution such that applying them to pattern yields observation. Used by tactics and rewriting:

///|
test "terms: pattern matching" {
  @types.Type::reset_table()
  @terms.Term::reset_table()
  let a = @types.mk_var("'a")
  let bool_ty = @types.bool_ty()
  let x = @terms.mk_var("x", a)
  let p = @terms.mk_var("p", bool_ty)

  // Match x:'a against p:bool => { x := p } and { 'a := bool }
  let (tm_s, ty_s) = x.match_term(p)
  assert_eq([..tm_s].length(), 1)
  assert_eq([..ty_s].length(), 1)
}

#Type Aliases

AliasExpands to
TermSubstSubst[Term, Term]
TermMatchResult(TermSubst, TypeSubst)

#
TermMatchResult

source

The result of pattern matching a term: a pair of a term substitution and a type substitution that, when applied to the pattern, yield the observation.

#
TermSubst

source

A substitution mapping terms to terms, used to replace free variables in a term.

#
Term

source
pub enum Term {
  FVar(String, 
Type)
  BVar(Int)
  Const(String, 
Type)
  App(Term, Term)
  Abs(Term, Term)
} derive(Compare, Eq, 
Debug)

HOL term in locally nameless representation: free variables are named, bound variables use de Bruijn indices, and constants carry their (possibly polymorphic) type.
impl Show for Term

#
Term::aconv

source
fn Term::aconv(self : Term, rhs : Term) -> Bool

Test alpha-equivalence: two terms are alpha-convertible if they are identical up to renaming of bound variables. Free variables and constants must match exactly.

#
Term::curry_eq

source
fn Term::curry_eq(self : Term) -> Term

Build the partially applied equality (=) : ty -> ty -> bool instantiated at self's type, then apply it to self, yielding a term of type ty -> bool. Used by derived equality rules.

#
Term::dest_abs

source
fn Term::dest_abs(self : Term) -> (Term, Term)

Decompose an abstraction Abs(x, body) back into (x', body') where x' is a fresh free variable and body' has every BVar(0) (and any residual free occurrence of x) replaced by x'.

Because the locally nameless encoding erases the original binder name, dest_abs must invent a fresh name that does not clash with any variable already present in the body. Starting from the annotation name it appends primes (') until the name is unused, guaranteeing that round-tripping mk_abs / dest_abs never accidentally captures a free variable.

This is the inverse of mk_abs: for any free variable x and term m, mk_abs(x, m).dest_abs() yields a pair (x', m') that is alpha-equivalent to (x, m).

Aborts if the term is not an abstraction.

#
Term::dest_eq

source
fn Term::dest_eq(tm : Term) -> (Term, Term) raise

Decompose an equation into its left- and right-hand sides, aborting if the term is not an equation.

#
Term::inst

source

Apply a type substitution to every type annotation in the term, specializing polymorphic constants and variables to concrete types.

#
Term::is_bool

source
fn Term::is_bool(self : Term) -> Bool

Test whether the term has boolean type.

#
Term::is_eq

source
fn Term::is_eq(tm : Term) -> Bool

Test whether the term is an equation of the form l = r.

#
Term::match_term

source

First-order pattern matching: find substitutions (sigma, tau) such that self.subst(sigma).inst(tau) == ob.

self is the pattern and ob is the observation (concrete term). Free variables in the pattern act as match variables — each one is bound to the corresponding sub-term of ob. Constants must match exactly (name and compatible type). Bound variables (de Bruijn indices) must be identical.

Returns a TermMatchResult = (TermSubst, TypeSubst):
  • The term substitution maps pattern variables to their matched sub-terms.
  • The type substitution maps type variables in the pattern to concrete types. Identity bindings (variable mapped to itself) are removed.

Aborts if the pattern cannot match the observation (structural mismatch, inconsistent variable binding, or type mismatch).

#
Term::mk_abs

source
fn Term::mk_abs(x : Term, m : Term) -> Term

Construct the abstraction \x. m in locally nameless encoding.

x must be a free variable (FVar). Every free occurrence of x inside m is replaced by BVar(0), and x itself is kept as a binder annotation so that dest_abs can recover a human-readable name. Under nested abstractions the de Bruijn index is shifted so that each BVar always points to its correct binder.

If x does not occur free in m, the body is left unchanged (a vacuous abstraction). If x is shadowed by an inner Abs with the same binder, occurrences below that inner binder are not captured.

Aborts if x is not a free variable.

#
Term::mk_const

source
fn Term::mk_const(name : String, ty : 
Type) -> Term raise

Construct a constant term, checking that the name is registered in the global signature and that the requested type is a valid instance of the declared polymorphic type.

#
Term::mk_eq

source
fn Term::mk_eq(lhs : Term, rhs : Term) -> Term

Build the equation lhs = rhs, checking that both sides have the same type and instantiating the polymorphic equality constant accordingly.

#
Term::new_const

source
fn Term::new_const(name : String, ty : 
Type) -> Term

Register a new constant with the given name and type in the global signature, aborting if the name is already in use. Returns the constructed constant term.

#
Term::pprint

source
fn Term::pprint(self : Term) -> String

Pretty-print the term followed by its type annotation, rendering bound variables by name and omitting internal constructors.

#
Term::reset_table

source
fn Term::reset_table() -> Unit

Reset the global constant table to the most recent checkpoint, discarding any constants registered since then.

#
Term::subst

source

Apply a term-level substitution simultaneously, replacing free variables according to the given mapping in a single pass.

Unlike sequential application (which would let the range of one pair be rewritten by later pairs), this looks up each free variable in the original term independently, matching standard HOL semantics.

#
Term::type_of

source
fn Term::type_of(self : Term) -> 
Type

Infer the type of a term by recursively traversing its structure.

#
const_

source
fn const_(name : String, ty : 
Type) -> Term

Construct a constant term without checking the global signature. Intended for the logic layer, which builds connective and type-operator heads before they are formally registered. Prefer mk_const for user-facing code.

#
mk_app

source
fn mk_app(m : Term, n : Term) -> Term

Construct a function application term.

#
mk_var

source
fn mk_var(name : String, ty : 
Type) -> Term

Construct a free (named) variable with the given name and type.

Source Files

Powered by MoonBit

Site sourceReport issuePackagesBuild queueSkillsStatistics

© 2026 mooncakes.io