package dedukti

  1. Overview
  2. Docs

Substitutions using DeBruijn indices.

exception UnshiftExn
type substitution = Basic.loc -> Basic.ident -> int -> int -> Term.term

A substitution is a function mapping a variable (location, identifier and DB index) under a given number of lambda abstractions to a term. A substitution raises Not_found meaning that the variable is not subsituted.

val apply_subst : substitution -> int -> Term.term -> Term.term

apply_subst subst n t applies subst to t under n lambda abstractions.

  • Variables with DB index k < n are considered "locally bound" and are never substituted.
  • Variables with DB index k >= n may be substituted if k-n is mapped in sigma.
val shift : int -> Term.term -> Term.term

shift i t shifts every De Bruijn indices in t by i.

val unshift : int -> Term.term -> Term.term

unshift i t shifts every De Bruijn indices in t by -i. Raises UnshiftExn when t contains De Bruijn variables of indices k <i.

val psubst_l : Term.term Stdlib.Lazy.t Basic.LList.t -> Term.term -> Term.term

psubst_l l k t substitutes the first n De Bruijn variables (with n = length l) in t with the corresponding term in l. Unshifts n times the free variables with greater indices.

val subst : Term.term -> Term.term -> Term.term

subst t u substitutes the first free De Bruijn variable with u in t. Unshifts the other free variables.

val subst_n : int -> Basic.ident -> Term.term -> Term.term

subst_n n y t substitutes the n-th free De Bruijn variable in t with a fresh variable named y becoming the first free variable in t. All others free variables are shifted by one preventing index collision.

val occurs : int -> Term.term -> bool

occurs n t returns true if t contains the variable n.