subst

Documentation

Overview

Package subst provides de Bruijn variable shifting and substitution.

This package is part of the trusted kernel and implements the fundamental operations on de Bruijn indexed terms. The algorithms follow Types and Programming Languages (TAPL) §6.2.

De Bruijn Indices

Variables are represented as indices rather than names:

• Index 0 refers to the innermost bound variable
• Index k refers to the variable bound by the k-th enclosing binder
• Free variables have indices >= context length

Shifting

Shift adjusts variable indices when opening/closing binders:

// Shift free variables by 1 (entering a binder)
shifted := subst.Shift(1, 0, term)

// Shift variables >= cutoff by d
shifted := subst.Shift(d, cutoff, term)

The cutoff parameter tracks binding depth - variables below the cutoff are bound and unchanged; variables at or above are shifted.

Substitution

Subst replaces a variable with a term:

// Replace variable 0 with s in t
result := subst.Subst(0, s, t)

Substitution automatically shifts the substituted term when entering binders to maintain correct indices.

Binder Handling

Both Shift and Subst increment the cutoff/index when entering binders:

• Pi, Lam, Sigma, Let - bind one variable
• Body positions have cutoff+1 or j+1

This ensures bound variables are never modified.

Interval Variables (Cubical)

Cubical type theory uses a separate namespace for interval variables:

• IShift - shifts interval variables (IVar indices)
• ISubst - substitutes interval terms for interval variables

These operate independently of term variable operations.

Face Formulas

Face formula versions handle the Face types:

• ShiftFace - shifts term variables in face formulas
• SubstFace - substitutes in face formulas
• IShiftFace - shifts interval variables in face formulas
• ISubstFace - substitutes interval terms in face formulas

Extension Points

Unknown term types are handled via extension functions:

• shiftExtension - for cubical and other extended terms
• substExtension - corresponding substitution

This allows the base implementation to support additional term types.

TAPL Reference

The implementation follows Pierce's "Types and Programming Languages":

• §6.2.1 - Shifting definition
• §6.2.2 - Substitution definition
• §6.2.3 - Properties and lemmas

Index

• func IShift(d, cutoff int, t ast.Term) ast.Term
• func IShiftFace(d, cutoff int, f ast.Face) ast.Face
• func ISubst(j int, s ast.Term, t ast.Term) ast.Term
• func ISubstFace(j int, s ast.Term, f ast.Face) ast.Face
• func Shift(d, cutoff int, t ast.Term) ast.Term
• func ShiftFace(d, cutoff int, f ast.Face) ast.Face
• func Subst(j int, s ast.Term, t ast.Term) ast.Term
• func SubstFace(j int, s ast.Term, f ast.Face) ast.Face

Functions

func IShift

func IShift(d, cutoff int, t ast.Term) ast.Term

IShift shifts all free interval variables >= cutoff by d positions. This operates in the interval variable namespace, separate from term variables.

func IShiftFace

func IShiftFace(d, cutoff int, f ast.Face) ast.Face

IShiftFace shifts interval variables in a face formula.

func ISubst

func ISubst(j int, s ast.Term, t ast.Term) ast.Term

ISubst substitutes interval term s for interval variable j in t. This operates in the interval variable namespace.

func ISubstFace

func ISubstFace(j int, s ast.Term, f ast.Face) ast.Face

ISubstFace substitutes an interval term for an interval variable in a face formula.

func Shift

func Shift(d, cutoff int, t ast.Term) ast.Term

Shift shifts all free de Bruijn variables >= cutoff by d positions. Follows TAPL §6.2.1.

func ShiftFace

func ShiftFace(d, cutoff int, f ast.Face) ast.Face

ShiftFace shifts term variables in a face formula (faces have no term vars).

func Subst

func Subst(j int, s ast.Term, t ast.Term) ast.Term

Subst substitutes s for variable j in t, adjusting indices. Follows TAPL §6.2.2.

func SubstFace

func SubstFace(j int, s ast.Term, f ast.Face) ast.Face

SubstFace substitutes a term for a term variable in a face formula.