Occurrence counting and family substitution

Term.occ

Work in a fixed sort type $S$, with an implicit signature $sig$ (which assigns to each arity list $w : \mathrm{List}\,S$ and each result sort $s : S$ a type $sig\,w\,s$ of operation symbols) and an implicit sorted family of variable types $X : S \to \mathrm{Type}$. A term of sort $s$ (an element of $\mathrm{Term}_{sig,X}(s)$) is either a variable $\mathrm{var}(x)$ with $x : X_s$, or an application $\mathrm{app}(\sigma, ts)$ with $\sigma : sig\,w\,s$ and $ts$ a vector of terms whose sorts are listed by $w$ (an element of $\mathrm{TermVec}_{sig,X}(w)$). The function Term.occ takes an implicit sort $v : S$, a distinguished variable $z : X_v$, an implicit sort $s : S$, and a term $P : \mathrm{Term}_{sig,X}(s)$, and returns a natural number, written here $\mathrm{occ}_z(P) \in \mathbb{N}$. It is defined by recursion on $P$:

• If $P = \mathrm{var}(x)$ with $x : X_s$: if the sorts satisfy $s = v$, take the proof $h : s = v$, transport $x$ along $h$ to get $h \triangleright x : X_v$, and return $1$ if $h \triangleright x = z$ and $0$ otherwise; if $s \neq v$, return $0$.
• If $P = \mathrm{app}(\sigma, ts)$: return $\mathrm{occ}_z(ts)$ using the TermVec version below; the operation symbol $\sigma$ itself contributes nothing.

Thus $\mathrm{occ}_z(P)$ counts the variable-leaf occurrences in $P$ that are exactly $z$ (matching both the sort $v$ and the value $z$). Equality of sorts and of elements of $X_v$ is decided classically (the definition is noncomputable and opens Classical).

TermVec.occ

With the same ambient data, TermVec.occ takes an implicit sort $v : S$, a distinguished variable $z : X_v$, an implicit arity list $w : \mathrm{List}\,S$, and a term vector $ts : \mathrm{TermVec}_{sig,X}(w)$ (either the empty vector $\mathrm{nil}$, or $\mathrm{cons}(t, ts')$ with $t$ a term and $ts'$ a shorter vector), returning a natural number. It is defined by recursion on $ts$:

• On the empty vector $\mathrm{nil}$: the value is $0$.
• On $\mathrm{cons}(t, ts')$: the value is $\mathrm{occ}_z(t) + \mathrm{occ}_z(ts')$, i.e. the occurrence count of $z$ in the head term $t$ plus the occurrence count of $z$ in the tail vector $ts'$.

So $\mathrm{occ}_z(ts)$ is the total number of occurrences of the variable $z$ across all component terms of the vector. It is noncomputable and uses classical decidability.

Term.substFamAux

With ambient $S$, $sig$, $X$ as above, Term.substFamAux takes an implicit sort $v : S$, a distinguished variable $z : X_v$, an implicit sort $s : S$, a term $P : \mathrm{Term}_{sig,X}(s)$, and a list $qs : \mathrm{List}\big(\mathrm{Term}_{sig,X}(v)\big)$ of candidate replacement terms of sort $v$. It returns an ordered pair whose first component is a term of $\mathrm{Term}_{sig,X}(s)$ and whose second component is a list in $\mathrm{List}\big(\mathrm{Term}_{sig,X}(v)\big)$ (the unconsumed remainder of $qs$). It is defined by recursion on $P$:

• If $P = \mathrm{var}(x)$ with $x : X_s$:
  • If $s = v$, with proof $h : s = v$:
    • If $h \triangleright x = z$:
      • If $qs$ is empty $[\,]$: return $(\mathrm{var}(x),\ [\,])$ — the variable is left unchanged and the empty list is returned.
      • If $qs = q :: qs'$: return $(h^{-1} \triangleright q,\ qs')$, where $h^{-1} : v = s$ and $q$ is transported along $h^{-1}$ to become a term of sort $s$; the remaining list is $qs'$ (one element consumed from the front).
    • If $h \triangleright x \neq z$: return $(\mathrm{var}(x),\ qs)$ — variable unchanged, list untouched.
  • If $s \neq v$: return $(\mathrm{var}(x),\ qs)$ — variable unchanged, list untouched.
• If $P = \mathrm{app}(\sigma, ts)$: compute $r := \mathrm{TermVec.substFamAux}\ z\ ts\ qs$, and return $(\mathrm{app}(\sigma,\ r_1),\ r_2)$, where $r_1$ is the substituted argument vector and $r_2$ is the leftover list from processing $ts$.

So this replaces occurrences of $z$ inside $P$ one at a time, each occurrence consuming the current head of the threaded list; if the list is exhausted an occurrence is left as $\mathrm{var}(x)$. It is noncomputable and uses classical decidability of the sort equality $s = v$ and of the equality $h \triangleright x = z$ in $X_v$.

TermVec.substFamAux

With the same ambient data, TermVec.substFamAux takes an implicit sort $v : S$, a distinguished variable $z : X_v$, an implicit arity list $w : \mathrm{List}\,S$, a term vector $ts : \mathrm{TermVec}_{sig,X}(w)$, and a list $qs : \mathrm{List}\big(\mathrm{Term}_{sig,X}(v)\big)$. It returns an ordered pair whose first component is a term vector in $\mathrm{TermVec}_{sig,X}(w)$ and whose second component is a list in $\mathrm{List}\big(\mathrm{Term}_{sig,X}(v)\big)$. It is defined by recursion on $ts$:

• On the empty vector $\mathrm{nil}$: return $(\mathrm{nil},\ qs)$ (nothing substituted, list unchanged).
• On $\mathrm{cons}(t, ts')$: first compute $r_1 := \mathrm{Term.substFamAux}\ z\ t\ qs$ (substitute into the head term $t$, threading the whole list $qs$); then compute $r_2 := \mathrm{TermVec.substFamAux}\ z\ ts'\ (r_1)_2$ (substitute into the tail vector $ts'$, threading the list left over from the head, namely $(r_1)_2$); finally return $\big(\mathrm{cons}((r_1)_1,\ (r_2)_1),\ (r_2)_2\big)$.

Consequently the replacement list is threaded strictly left-to-right and depth-first: within a $\mathrm{cons}$, the head term is fully processed before the tail; within an $\mathrm{app}$ (via Term.substFamAux), the argument vector is processed in this same order. Each successive occurrence of $z$ takes the next element from the front of the list, and once the list is empty every further occurrence of $z$ is kept unchanged; all non-$z$ leaves and all operation nodes are rebuilt identically. It is noncomputable.

substFam

With ambient $S$, $sig$, $X$ as above, substFam takes two implicit sorts $v, s : S$, a distinguished variable $z : X_v$, a term $P : \mathrm{Term}_{sig,X}(s)$, and a family

$$qs : \mathrm{Fin}\big(\mathrm{occ}_z(P)\big) \longrightarrow \mathrm{Term}_{sig,X}(v),$$

that is, a replacement term of sort $v$ for each index $i$ with $0 \le i < \mathrm{occ}_z(P)$, where $\mathrm{occ}_z(P) = \mathrm{Term.occ}\ z\ P$ is the occurrence count defined above. It returns a term of $\mathrm{Term}_{sig,X}(s)$, defined as the first component of

$$\mathrm{Term.substFamAux}\ z\ P\ \big(\mathrm{ofFn}(qs)\big),$$

where $\mathrm{ofFn}(qs) = \big[\,qs(0),\ qs(1),\ \dots,\ qs(\mathrm{occ}_z(P) - 1)\,\big]$ is the list of the family's values taken in index order (of length exactly $\mathrm{occ}_z(P)$). The second component returned by $\mathrm{Term.substFamAux}$ (the unconsumed tail) is discarded. By the threading described above, the result is $P$ with its $i$-th occurrence of $z$ (in the left-to-right depth-first traversal order) replaced by $qs(i)$, for each $i$. Degenerate case: if $\mathrm{occ}_z(P) = 0$, then $\mathrm{Fin}(0)$ is empty, $qs$ is the empty family, $\mathrm{ofFn}(qs) = [\,]$, and the output is $P$ (rebuilt without any change). The definition is noncomputable and relies on classical decidability of equality on $S$ and on $X_v$.