This article is obsolete. It has been superseded by https://doi.org/10.47757/abstraction.logic.2.

Abstraction Logic

Cite as: https://doi.org/10.47757/abstraction.logic.1

Oct 22, 2021

Abstract

Abstraction Logic is introduced as a foundation for Practical Types [1] and Practal [2]. It combines the simplicity of ﬁrst-order logic with direct support for variable binding constants called abstractions. It also allows free variables to depend on parameters, which means that ﬁrst-order axiom schemata can be encoded as simple axioms. Conceptually abstraction logic is situated between ﬁrst-order logic and second-order logic. It is sound and complete with respect to an intuitive and simple algebraic semantics.

Introduction

The goal of Practical Types [1] is to provide a foundation for formal machine-assisted reasoning that anyone would ﬁnd empowering who is interested in rigorous thinking and design. This paper provides a foundation on which Practical Types will be built as a particular class of abstraction logics.

Like ﬁrst-order logic, abstraction logic has a single universe of discourse, i.e. it is one-sorted. It goes even further than ordinary ﬁrst-order logic in that truth values are part of this universe, i.e. the universe forms a Fregean domain [3].

Like higher-order logic and type theory, abstraction logic provides built-in support for variable binding constructs. But variable binding is not achieved indirectly via a function sort or type; instead it is directly modelled via shape speciﬁcations for (possibly) variable binding constructs called abstractions. Abstractions are simply the constants of abstraction logic. As a consequence

\alpha

-equivalence of terms is a central concept in abstraction logic, but

\beta/\eta

-conversion do not play any role at this level.

Free variables can depend on parameters. Thus where ﬁrst-order logic needs axiom schemata consisting of inﬁnitely many axioms, abstraction logic can express the same with a single axiom, just like higher-order logic. This is illustrated multiple times when we present several concrete abstraction logics →.

Although abstraction logic started out as an investigation into the logic of Practical Types, it will be important for the design of Practal [2] in its own right. The relationship between Practal, Practical Types and abstraction logic is similar to the relationship between the Isabelle System [4] and its logics HOL and Pure. Locales [5] are an important mechanism for modular reasoning in Isabelle built on top of Pure. Because abstraction logic is simpler than type theory, but at the same time more versatile, the same should be true for an abstraction logic mechanism for modular reasoning inspired by locales.

The relationship between Practical Types and abstraction logic can also be compared to the relationship between set theory and ﬁrst-order logic. Similarly, abstraction logic is not limited to Practical Types, it can provide a foundation for many applications where currently ﬁrst-order logic is used. Furthermore, abstraction logic can be applied in places where previously higher-order logic was needed, as in the realm of interactive theorem proving.

Overview. We ﬁrst list some notation →. Then abstraction algebras → are introduced. Then the syntax → and semantics → of terms representing values in abstraction algebras is presented. De Bruijn terms → for abstraction syntax are deﬁned next, and the treatment of $\alpha$ -equivalence → is based on them. After introducing substitution →, we show that de Bruijn terms form an abstraction algebra themselves →, and use this fact to show the fundamental role that

\alpha

-equivalence plays. Finally abstraction logic → itself is introduced, and our notion of proof → is shown to be sound →. Several examples → of abstraction logics are presented. We discuss consistency → in the context of abstraction logic. We construct the Rasiowa Abstraction Algebra → of any abstraction logic

{\mathcal{L}}

that extends Deduction Logic with Equality →, and use it to prove completeness → of any such

{\mathcal{L}}

, including intuitionistic and classical abstraction logic. We conclude by brieﬂy discussing matching and uniﬁcation → of abstraction syntax terms.

Preliminaries

Let’s ﬁx some general notation ﬁrst:

$\mathbb{N}$ is the set of natural numbers starting from $0$ .
We write ${\overline{{n}}}$ for $\{0,\ldots,n-1\}$ , in particular ${\overline{{0}}} = \emptyset$ .
We write ${\langle {i_0, \ldots, i_{n-1}} \rangle}$ where $i_0 < i_1 < \ldots < i_{n-1}$ for the set $\{{i_0, \ldots, i_{n-1}}\}$ .
We write ${U \rightarrow V}$ for the set of functions from set $U$ to set $V$ .
We write ${U ↪ V}$ for the set of partial functions from set $U$ to set $V$ .
The function $\operatorname{id}_{U} : {U \rightarrow U}$ denotes the identity on $U$ .
We write $U \times V$ for the cartesian product of the sets $U$ and $V$ .
We deﬁne $U^n$ for $n \in \mathbb{N}$ , $n \geq 1$ via $U^1 = U$ and $U^{m+1} = U^m \times U$ for $m \geq 1$ .
We write ${|p|}$ for the size of the ﬁnite set $p$ .
For $f : {U \rightarrow V}$ , distinct ${x_0, \ldots, x_{n-1}}$ , and arbitrary ${v_0, \ldots, v_{n-1}}$ in $V$ , we write $f[x_0 \coloneqq v_0, \ldots, x_{n-1} \coloneqq v_{n-1}]$ for the function $g : {{U \cup \{{x_0, \ldots, x_{n-1}}\}} \rightarrow V}$ deﬁned via $g(u) = \begin{cases} v_i & \text{if}\ u = x_i \\ f(u) & \text{if}\ u \notin \{{x_0, \ldots, x_{n-1}}\} \end{cases}$
Instead of $f[x_{i_0} \coloneqq v[i_0], \ldots, x_{i_{n-1}} \coloneqq v[i_{n-1}]]$ we also write $f[\overline{x_p \coloneqq v[p]}]$ where $p = {\langle {i_0, \ldots, i_{n-1}} \rangle}$ and $v[x]$ stands for an arbitrary expression depending on $x$ .

Algebra

A shape

\sigma

prescribes a number

m

of binders and a number

n

of parameters. Furthermore it assigns to each parameter the set of binders it depends on. A shape is therefore written as

(m; p_0, \ldots, p_{n-1})

where

m, n \in \mathbb{N}

, and each

p_i

is a subset of

{\overline{{m}}}

. Furthermore we require that there are no superﬂuous binders:

\bigcup_{i=0}^{n-1} p_i = {\overline{{m}}}

We call

m

the valence of the shape, and

n

its arity. Above condition implies that a shape with arity

0

necessarily has valence

0

. It also implies that for a unary shape its sole parameter will depend on all binders.

An abstraction signature

\mathfrak{S} = (a_0 : \sigma_0, \ldots, a_{k-1} : \sigma_{k-1})

is a list of

k

different abstractions

a_i

, where each abstraction

a_i

is associated with its shape

\sigma_i

An abstraction algebra

{\mathfrak{A}} = (U; I; \mathfrak{S})

is a non-empty set

U

together with an abstraction signature

\mathfrak{S}

and an interpretation

I

which interprets an abstraction

a_i

as an element

I(a_i)

of the set

{\Lambda_{U}({\sigma_i})}

. The set

{\Lambda_{U}({\sigma_i})}

will be deﬁned shortly.

Examples of abstractions and their shapes are:

Equality $x = y$ has two parameters $x$ and $y$ and no binders. The shape of equality is therefore ${\sigma_{=}} = (0; \{\}, \{\})$ .
Universal quantiﬁcation $\forall x.\, P[x]$ has one binder $x$ and one parameter $P$ , which depends on $x$ . The shape of universal quantiﬁcation is ${\sigma_{{\forall}}} = (1; \{0\})$ .
Function abstraction $\lambda x : T.\, A[x]$ has one binder $x$ and two parameters $T$ and $A$ . The parameter $T$ does not depend on $x$ , but $A$ does. The shape of function abstraction is therefore ${\sigma_{{\lambda}}} = (1; \{\}, \{0\})$ .

We require an abstraction

a

of shape

\sigma

to be an element of

{\Lambda_{U}({\sigma})}

. We deﬁne

{\Lambda_{U}({\sigma})}

for

\sigma = (m; {p_0, \ldots, p_{n-1}})

as follows:

{\Lambda_{U}({\sigma})} = \begin{cases} U & \text{if}\ n = 0\\ {{{\mathcal{F}_{m}^{{p_0}}(U)} \times \ldots \times {\mathcal{F}_{m}^{{p_{n-1}}}(U)}} \rightarrow U} & \text{if}\ n \geq 1 \end{cases}

Here, for

m \geq 1

and

p \subseteq {\overline{{m}}}

, we deﬁne

{\mathcal{F}_{m}^{p}(U)}

as follows:

{\mathcal{F}_{m}^{p}(U)} = \begin{cases} U & \text{if}\ p = \emptyset\\ \{\, f \circ {\pi_m^p(U)} \,\mid\, f \in {{U^{{|p|}}} \rightarrow U} \} \subseteq {{U^m} \rightarrow U} & \text{if}\ p \neq \emptyset \end{cases}

The projections

{\pi_m^p(U)} : {{U^m} \rightarrow {U^{|{p}|}}}

are deﬁned for

p = {\langle {i_0, \ldots, i_{n-1}} \rangle}

via

(u_0, \ldots, u_{m-1}) \mapsto (u_{i_0}, \ldots, u_{i_{n-1}})

In particular, if the valence of

\sigma

0

and its arity

n

, then

{\Lambda_{U}({\sigma})} = \begin{cases} U & \text{if}\ n = 0\\ {{U^n} \rightarrow U} & \text{if}\ n \neq 0 \end{cases}

Note that an abstract algebra as described by Rasiowa [6] (see also [7], [8] →) is thus simply an abstraction algebra where all abstractions have zero valence.

If the valence of

\sigma

1

, then

{\Lambda_{U}({\sigma})} = {{{\mathcal{F}_{1}^{{p_0}}(U)} \times \ldots \times {\mathcal{F}_{1}^{{p_{n-1}}}(U)}} \rightarrow U}

, where

{\mathcal{F}_{1}^{{p_i}}(U)}

is either

U

{U \rightarrow U}

, depending on whether

p_i = \emptyset

p_i = \{0\}

, respectively.

Continuing our previous examples, we can now say the following:

The interpretation of $=$ is a function in ${{U \times U} \rightarrow U}$ .
The interpretation of $\forall$ is a function in ${{({U \rightarrow U})} \rightarrow U}$ .
The interpretation of $\lambda$ is a function in ${{U \times ({U \rightarrow U})} \rightarrow U}$ .

Bounded universal quantiﬁcation

\forall x : T.\, P[x]

has shape

(1; \{\}, \{0\})

, and is therefore interpreted as an element of

{{U \times ({U \rightarrow U})} \rightarrow U}

Another example is deﬁned by

\operatorname{funeq} x.\, T\, f[x]\, g[x] ≝ \forall x : T.\, f[x] = g[x]

The shape of

\operatorname{funeq}

(1; \{\}, \{0\}, \{0\})

, and therefore

\operatorname{funeq} : {{U \times ({U \rightarrow U}) \times ({U \rightarrow U})} \rightarrow U}

Syntax

Given an abstraction signature

\mathfrak{S} = (a_0 : \sigma_0, \ldots, a_{k-1} : \sigma_{k-1})

and a set of variables

X

, we deﬁne the set

{\mathcal{T}_{{X}}({\mathfrak{S}})}

of terms over

\mathfrak{S}

. We require variables and abstractions not to overlap, of course, i.e.

a_i \notin X

for all

i \in {\overline{{k}}}

. We also require each variable

x\in X

to be associated with a ﬁxed arity

{x_{\operatorname{arity}}} \in \mathbb{N}

The set

{\mathcal{T}_{{X}}({\mathfrak{S}})}

of terms is then deﬁned inductively as follows:

Given a variable $x$ and terms ${t_0, \ldots, t_{{{x_{\operatorname{arity}}}}-1}}$ , $x[{t_0, \ldots, t_{{{x_{\operatorname{arity}}}}-1}}]$ is a term. We also write just $x$ instead of $x[\,]$ .
Given an abstraction $a$ of valence $m$ and arity $n$ , terms ${t_0, \ldots, t_{n-1}}$ , and distinct variables ${x_0, \ldots, x_{m-1}}$ such that ${{(x_i)}_{\operatorname{arity}}} = 0$ for all $i \in {\overline{m}}$ , $(a\,x_0 \ldots x_{m-1}.\, t_0 \ldots t_{n-1})$ is also a term.

Note that with this deﬁnition all terms in

{\mathcal{T}_{{X}}({\mathfrak{S}})}

are wellformed, although the deﬁnition makes only use of the valence and arity of an abstraction instead of its full shape. Of course, the full shape is important: it is needed to determine the free variables

{\operatorname{Free}({t})}

of a term

t \in {\mathcal{T}_{{X}}({\mathfrak{S}})}

. We deﬁne

{\operatorname{Free}(t)}

recursively, following the inductive deﬁnition of

{\mathcal{T}_{{X}}({\mathfrak{S}})}

\begin{array}{lcl} {\operatorname{Free}({x[{t_0, \ldots, t_{{{x_{\operatorname{arity}}}}-1}}]})} & = & \{x\} \cup {\operatorname{Free}({t_0})} \cup \ldots \cup {\operatorname{Free}({t_{{x_{\operatorname{arity}}} - 1}})} \\[0.2cm] {\operatorname{Free}({(a\,x_0 \ldots x_{m-1}.\, t_0 \ldots t_{n-1})})} & = & \phantom{\cup\ }({\operatorname{Free}({t_0})} \setminus \{x_{i_{0, 0}}, \ldots, x_{i_{0, {|{p_0}|} - 1}}\}) \\ & &\cup\ ({\operatorname{Free}({t_1})} \setminus \{x_{i_{1, 0}}, \ldots, x_{i_{1, {|{p_1}|} - 1}}\}) \\ & & \vdots \\ & &\cup\ ({\operatorname{Free}({t_{n-1}})} \setminus \{x_{i_{n-1, 0}}, \ldots, x_{i_{n-1, {|{p_{n-1}}|} - 1}}\}) \\ & & \text{where}\ {\sigma_{a}} = (m; {p_0, \ldots, p_{n-1}}) \\ & & \text{and}\ p_j = \langle i_{j, 0}, \ldots, i_{j, {|{p_j}|} - 1} \rangle \ \forall j \in {\overline{{n}}} \end{array}

In case of

{\operatorname{Free}(t)} = \emptyset

, the term

t

is called closed.

The following table examines our previous examples in terms of abstraction syntax:

\begin{array}{c|c|c} {\includegraphics[height=0.5em]{A10D021D-5882-44D4-B25D-23270BF7F086}} & {\includegraphics[height=0.5em]{7E37D7C6-876D-42D0-97EF-4EA4FA1B0387}} & {\includegraphics[height=0.5em]{9EFF3EE0-A68A-4915-BD4B-1C43A740F06C}} \\\hline x = y & (= .\, x\ y) & x, y \\ \forall x.\, P[x] & (\forall x.\, P[x]) & P \\ \lambda x : T.\, A[x] & (\lambda x .\, T\, A[x]) & T, A \\ \forall x : T.\, P[x] & (\forall x.\, T\, P[x]) & T, P \\ \operatorname{funeq} x.\, T\, f[x]\, g[x] & (\operatorname{funeq} x.\, T\, f[x]\, g[x]) & T, f, g\\ \forall x : T.\, f[x] = g[x] & (\forall x.\, T\, (= .\, f[x]\, g[x])) & T, f, g \end{array}

Note that

x

is a free variable of the expression

\lambda x : x.\ x

Although the variable

x

is bound in the second parameter of

\lambda

, it occurs free in the ﬁrst parameter of

\lambda

, and is therefore a free variable of the entire expression.

Semantics

Given a set

F

of variables, and a set

U

, a valuation

\nu

F

U

is a mapping that assigns to each

x \in F

with

{x_{\operatorname{arity}}} = 0

an element

\nu(x) \in U

, and to each

x \in F

with

{x_{\operatorname{arity}}} \geq 1

a function

\nu(x) \in {{U^{{x_{\operatorname{arity}}}}} \rightarrow U}

. We denote the set of valuations of

F

U

{\includegraphics[height=0.5em]{E58E2822-8758-4F64-8D6D-B65CBBD65A47}}(F, U)

Let

\mathfrak{S}

be an abstraction signature, and

{\mathfrak{A}} = (U; I; \mathfrak{S})

an abstraction algebra with signature

\mathfrak{S}

. Given a term

t \in {\mathcal{T}_{X}({\mathfrak{S}})}

, any valuation

\nu

{\operatorname{Free}(t)}

U

determines an element

{\nu}\llbracket{t}\rrbracket \in U

, recursively deﬁned as follows:

If $t = x[{t_0, \ldots, t_{{{x_{\operatorname{arity}}}}-1}}]$ , then $x \in {\operatorname{Free}(t)}$ , and ${\operatorname{Free}({t_i})} \subseteq {\operatorname{Free}(t)}$ for all $i \in {\overline{{{x_{\operatorname{arity}}}}}}$ . Thus we set ${\nu}\llbracket{t}\rrbracket = \begin{cases} \nu(x) & \text{if}\ {x_{\operatorname{arity}}} = 0\\ \nu(x)\left({\nu}\llbracket{{t_0}}\rrbracket, \ldots, {\nu}\llbracket{{t_{{x_{\operatorname{arity}}} - 1}}}\rrbracket\right) & \text{if}\ {x_{\operatorname{arity}}} \geq 1 \end{cases}$
If $t = (a.\, t_0 \ldots t_{n-1})$ for an abstraction $a$ with zero valence and arity $n$ , we set ${\nu}\llbracket{t}\rrbracket = \begin{cases} I(a) & \text{if}\ n = 0\\ I(a)\left({\nu}\llbracket{{t_0}}\rrbracket, \ldots, {\nu}\llbracket{{t_{n - 1}}}\rrbracket\right) & \text{if}\ n \geq 1 \end{cases}$
Assume now $t = (a\,x_0 \ldots x_{m-1}.\, t_0 \ldots t_{n-1})$ for an abstraction $a$ with valence $m \geq 1$ and arity $n \geq 1$ , and of shape ${\sigma_{{a}}} = (m; {p_0, \ldots, p_{n-1}})$ . Let us consider a ﬁxed $i \in {\overline{{n}}}$ , and let $p_i = {\langle {j_0, \ldots, j_{k-1}} \rangle} \subseteq {\overline{m}}$ . We have ${\operatorname{Free}({t_i})} \subseteq {\operatorname{Free}(t)} \cup \{x_{j_0}, \ldots, x_{j_{k-1}}\}$ Therefore, for any $({u_0, \ldots, u_{m-1}}) \in U^m$ , the valuation $\mu_i = \nu[x_{j_0} \coloneqq u_{j_0}, \ldots, x_{j_{k-1}} \coloneqq u_{j_{k-1}}]$ determines a value ${\mu_i}\llbracket{{t_i}}\rrbracket \in U$ . Deﬁning $f_i : {{U^m} \rightarrow U}$ by $f_i : ({u_0, \ldots, u_{m-1}}) \mapsto {\mu_i}\llbracket{{t_i}}\rrbracket$ it is obvious that $f_i \in {\mathcal{F}_{m}^{{p_i}}(U)}$ . Consequently, we set ${\nu}\llbracket{t}\rrbracket = I(a)\left({f_0, \ldots, f_{n-1}}\right)$

t

is a closed term, then

{\nu}\llbracket{t}\rrbracket

is independent of the choice of the valuation

\nu

U

, and we can therefore deﬁne

{{\llbracket t \rrbracket}_{{\mathfrak{A}}}} = {\nu}\llbracket{t}\rrbracket

De Bruijn Terms

Terms

{\mathcal{T}_{{X}}({\mathfrak{S}})}

provide an adequate user interface for humans, but are awkward to handle from a technical point of view. This becomes apparent when formulating more complex operations on terms, like substitution. One reason for this awkwardness is the potential of clashes between bound variables and free variables. Another reason is that two terms which are semantically equivalent, like

(a\, x.\, x)

and

(a\, y.\, y)

, can nevertheless be syntactically different because of different choices for the names of bound variables.

In actual software implementations of logic, a common approach to deal with this problem is called locally nameless [9]. The following deﬁnitions are inspired by this approach. We ﬁrst deﬁne de Bruijn preterms

{\mathcal{B}_{{X}}^{\text{pre}}({\mathfrak{S}})}

For any $n \in \mathbb{N}$ , $\uparrow\hspace{-0.15em}{{n}}$ is a de Bruijn preterm. We implicitly assume everywhere that $\uparrow\hspace{-0.15em}{{n}} \notin X$ . Given a set $N \subset \mathbb{N}$ we write $\uparrow\hspace{-0.15em}{{N}}$ for the set $\{\uparrow\hspace{-0.15em}{{n}} \mid n \in N\}$ .
Given a variable $x \in X$ and de Bruijn preterms ${t_0, \ldots, t_{{{x_{\operatorname{arity}}}}-1}}$ , $x[{t_0, \ldots, t_{{{x_{\operatorname{arity}}}}-1}}]$ is a de Bruijn preterm. We also write just $x$ instead of $x[\,]$ .
Given an abstraction $a$ of arity $n$ , and de Bruijn preterms ${t_0, \ldots, t_{n-1}}$ , $(a\,t_0 \ldots t_{n-1})$ is also a de Bruijn preterm.

The idea is that a term like

(a\, x\, y.\, (b.\, x\, y)\, (c\, x.\, x\, y))

corresponds to the de Bruijn term

(a\, (b\, \uparrow\hspace{-0.15em}{{0}}\, \uparrow\hspace{-0.15em}{{1}})\, (c\, \uparrow\hspace{-0.15em}{{0}}\, \uparrow\hspace{-0.15em}{{2}}))

This correspondence is made precise by the mapping

\alpha : {{{\mathcal{T}_{{X}}({\mathfrak{S}})}} \rightarrow {{\mathcal{B}_{{X}}^{\text{pre}}({\mathfrak{S}})}}}

Let

X_0 = \{x \in X \mid {{x}_{\operatorname{arity}}} = 0\}

. To deﬁne

\alpha

, we ﬁrst deﬁne a function

\alpha' : {{{\mathcal{T}_{{X}}({\mathfrak{S}})} \times ({{X_0} ↪ {\mathbb{N}}})} \rightarrow {{\mathcal{B}_{{X}}^{\text{pre}}({\mathfrak{S}})}}}

which keeps track of the current mapping of bound variables to de Bruijn indices:

\begin{array}{rcl} \alpha'(x[{t_0, \ldots, t_{n-1}}], \eta) & = & x[\alpha'(t_0, \eta), \ldots, \alpha'(t_{n - 1}, \eta)] \\ & & \text{if}\ \eta\ \text{is undefined at}\ x \\[0.5em] \alpha'(x, \eta) & = & \uparrow\hspace{-0.15em}{{\eta(x)}} \\ & & \text{if}\ \eta\ \text{is defined at}\ x\\[0.5em] \alpha'((a\,x_0 \ldots x_{m-1}.\, t_0 \ldots t_{n-1}), \eta) & = & (a\, t'_0 \ldots t'_{n-1}) \\ \text{where the shape of}\ a &=& (m; {p_0, \ldots, p_{n-1}}) \\ \text{and for all }\ i \in {\overline{{n}}},\ t'_i & = & \alpha'(t_i, (\eta + m)[\overline{x_{p_i} \coloneqq p_i}]) \end{array}

For any partial function

f : {U ↪ {\mathbb{N}}}

and any

m \in \mathbb{N}

we deﬁne

f' = f + m

in the obvious way such that

f'(u) = f(u) + m

holds if

f

is deﬁned at

u \in U

Then we can deﬁne

\alpha

\alpha(t) = \alpha'(t, \emptyset)

Of particular interest are those elements of

{\mathcal{B}_{{X}}^{\text{pre}}({\mathfrak{S}})}

that are in the image of

\alpha

. We are also interested in (part of) the image of

\alpha'

\begin{array}{rcl} {\mathcal{B}_{{X}}^{h}({\mathfrak{S}})} & = & \left\{ \alpha'(t, \eta) \mid (t, \eta) \in {\mathcal{T}_{{X}}({\mathfrak{S}})} \times ({{X_0} ↪ {{\overline{h}}}}) \right\} \\[0.5em] {\mathcal{B}_{{X}}({\mathfrak{S}})} & = & \bigcup_{h = 0}^\infty\, {\mathcal{B}_{{X}}^{h}({\mathfrak{S}})} \end{array}

The image of

\alpha

therefore is

{\mathcal{B}_{{X}}^{0}({\mathfrak{S}})}

. We call

{\mathcal{B}_{{X}}({\mathfrak{S}})}

the set of de Bruijn terms, and

{\mathcal{B}_{{X}}^{h}({\mathfrak{S}})}

is the set of de Bruijn terms with at most

h

holes.

Instead of deﬁning de Bruijn terms indirectly via

\alpha'

, it is easy to carve them out of de Bruijn preterms in a more direct fashion. For that we need the notion of free atoms

{\operatorname{FreeAtoms}(t)}

of a de Bruijn preterm

t \in {\mathcal{B}_{{X}}^{\text{pre}}({\mathfrak{S}})}

\begin{array}{rcl} {\operatorname{FreeAtoms}(t)} & = & {\operatorname{FreeAtoms}_{0}(t)} \\[0.5em] {\operatorname{FreeAtoms}_{l}({\uparrow\hspace{-0.15em}{n}})} & = & \begin{cases} \emptyset & \text{if}\ n < l\\ \{n - l\} & \text{if}\ n \geq l \end{cases}\\[1.5em] {\operatorname{FreeAtoms}_{l}({x[{t_0, \ldots, t_{n-1}}]})} & = & \{x\} \cup \bigcup_{i=0}^{n-1} {\operatorname{FreeAtoms}_{l}({t_i})} \\[0.8em] {\operatorname{FreeAtoms}_{l}({(a\,t_0\ldots t_{n-1})})} & = & \bigcup_{i=0}^{n-1} {\operatorname{FreeAtoms}_{{l + m}}({t_i})} \\ & & \text{where}\ m\ \text{is the valence of}\ a \end{array}

De Bruijn terms

{\mathcal{B}_{{X}}({\mathfrak{S}})}

are then those de Bruijn preterms

t

such that for every subpreterm of

t

of the form

(a\,t_0 \ldots t_{n-1})

the inclusion

{\operatorname{FreeAtoms}({t_i})}\, \cap \uparrow\hspace{-0.15em}{{{\overline{m}}}} \subseteq\, \uparrow\hspace{-0.15em}{{p_i}}

holds for all

i \in {\overline{n}}

. Here the shape of

a

(m; {p_0, \ldots, p_{n-1}})

Note that an immediate consequence of this characterisation is that every subterm of a de Bruijn term is also a de Bruijn term.

Furthermore, note that

{\mathcal{B}_{{X}}^{h}({\mathfrak{S}})} = \left\{ t \in {\mathcal{B}_{{X}}({\mathfrak{S}})} \mid {\operatorname{FreeAtoms}(t)}\,\cap \uparrow\hspace{-0.15em}{{\mathbb{N}}} \subseteq\, \uparrow\hspace{-0.15em}{{{\overline{h}}}} \right\}

$\alpha$ -Equivalence

We say that two terms

s

and

t

{\mathcal{T}_{{X}}({\mathfrak{S}})}

are $\alpha$ -equivalent iff

\alpha(s) = \alpha(t)

The importance of

\alpha

-equivalence stems from the fact that it is the same as semantical equivalence. We call

s

and

t

{\mathcal{T}_{{X}}({\mathfrak{S}})}

semantically equivalent iff for any abstraction algebra

(U; I; \mathfrak{S})

, and for any valuation

\nu \in {\includegraphics[height=0.5em]{EA73FE70-E33E-4531-B01C-8C47083D2BFD}}({X}, U)

, we have

\nu(s) = \nu(t)

We ﬁrst show that

\alpha

-equivalence implies semantical equivalence.

To this end, we deﬁne valuations also on de Bruijn terms. Given a set

F

of variables and a subset

N

\mathbb{N}

, a de Bruijn valuation

\nu

F\, \cup \uparrow\hspace{-0.15em}{{N}}

U

is a mapping such that

\nu

is a valuation of

F

U

, and additionally,

\nu

assigns to each

\uparrow\hspace{-0.15em}{{n}}

an element

\nu(\uparrow\hspace{-0.15em}{{n}}) \in U

for all

n \in N

Any valuation

\nu

{\operatorname{FreeAtoms}({t})}

U

determines an element

{\nu}\llbracket{t}\rrbracket \in U

\begin{array}{rcl} {\nu}\llbracket{{\uparrow\hspace{-0.15em}{n}}}\rrbracket & = & \nu(\uparrow\hspace{-0.15em}{n}) \\[0.5em] {\nu}\llbracket{{x[{t_0, \ldots, t_{n-1}}]}}\rrbracket & = & \nu(x)({\nu}\llbracket{{t_0}}\rrbracket, \ldots, {\nu}\llbracket{{t_{n-1}}}\rrbracket)\\[0.5em] {\nu}\llbracket{{(a\,t_0\ldots t_{n-1})}}\rrbracket & = & I(a)({\nu}\llbracket{{t_0}}\rrbracket, \ldots, {\nu}\llbracket{{t_{n-1}}}\rrbracket)\\ & & \text{if the valence of}\ a\ \text{is}\ 0 \\[0.5em] {\nu}\llbracket{{(a\,t_0\ldots t_{n-1})}}\rrbracket & = & I'(a)(f_0, \ldots, f_{n-1})\\ & & \text{if the valence of}\ a\ \text{is}\ m \geq 1 \\ \text{where}\ f_i({u_0, \ldots, u_{m-1}})& = & {\uparrow^{m}\hspace{-0.15em}({\nu})[\uparrow\hspace{-0.15em}{{0}} \coloneqq u_0, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq u_{m-1}]}\llbracket{{t_i}}\rrbracket\\ & & \text{for all}\ ({u_0, \ldots, u_{m-1}}) \in U^m \end{array}

Here

I'

is a slight modiﬁcation of the interpretation

I

in that where

I(a)

expects an element

e \in U

as one of its arguments,

I'(a)

will accept a constant function

({u_0, \ldots, u_{m-1}}) \mapsto e

instead. Otherwise,

I'

and

I

are identical.

The valuation

\uparrow^{m}\hspace{-0.15em}({\nu})

is derived from

\nu

via

\begin{array}{rcll} \uparrow^{m}\hspace{-0.15em}({\nu})(x) & = & \nu(x) & \text{where}\ x \in X \\ \uparrow^{m}\hspace{-0.15em}({\nu})(\uparrow\hspace{-0.15em}{{(m + n)}}) & = & \nu(\uparrow\hspace{-0.15em}{n}) & \text{where}\ n \in \mathbb{N} \end{array}

In the above the left hand sides are deﬁned iff the right hand sides are deﬁned.

It is not immediately obvious that

{\nu}\llbracket{{(a\,t_0\ldots t_{n-1})}}\rrbracket

is well-deﬁned, because in order to be able to apply

I'(a)

({f_0, \ldots, f_{n-1}})

, the

f_i

cannot be just any functions in

{{U^m} \rightarrow U}

. Assuming that the shape of

a

(m; {p_0, \ldots, p_{n-1}})

, if

p_i = \emptyset

f_i

must be a constant function, and for

p_i \neq \emptyset

f_i

needs to be in

{\mathcal{F}_{m}^{{p_i}}(U)}

. But this is easily seen to be the case, given that

{\nu'}\llbracket{t}\rrbracket \neq {\nu}\llbracket{t}\rrbracket

only holds if

\nu'

and

\nu

have a different assignment for some

q \in {\operatorname{FreeAtoms}(t)}

, and according to our earlier observation →,

{\operatorname{FreeAtoms}({t_i})}\, \cap \uparrow\hspace{-0.15em}{{{\overline{m}}}} \subseteq\, \uparrow\hspace{-0.15em}{{p_i}}

Given a valuation

\nu \in {\includegraphics[height=0.5em]{59D36504-10AA-4132-A799-7F0B72E08685}}({X}, U)

, together with an injective function

\eta : {{X_0} ↪ {\mathbb{N}}}

, the corresponding de Bruijn valuation

\nu_\eta

is deﬁned as

\begin{array}{rcll} \nu_\eta(x) & = & \nu(x) & \text{where}\ x \in X \\ \nu_\eta(\uparrow\hspace{-0.15em}{n}) & = & \nu(x) & \text{where}\ \eta(x) = n \end{array}

We prove that for any term

t \in {\mathcal{T}_{{X}}({\mathfrak{S}})}

, any valuation

\nu \in {\includegraphics[height=0.5em]{573C560E-B7CF-40F0-91DA-F89AEBAB3EFB}}({X}, U)

, and any injective

\eta : {{X_0} ↪ {\mathbb{N}}}

, we have

{\nu_\eta}\llbracket{{\alpha'(t, \eta)}}\rrbracket = {\nu}\llbracket{t}\rrbracket\quad

The proof is by induction over

t

Assume $t = x[{t_0, \ldots, t_{n-1}}]$ . Then ${\nu}\llbracket{t}\rrbracket = \nu(x)({\nu}\llbracket{{t_0}}\rrbracket, \ldots, {\nu}\llbracket{{t_{n-1}}}\rrbracket)$ .
- If $\eta$ is undeﬁned at $x$ then $t' = \alpha'(t, \eta) = x[\alpha'(t_0, \eta), \ldots, \alpha'(t_{n - 1}, \eta)]$ and furthermore, $\begin{array}{rcl} {\nu_\eta}\llbracket{{t'}}\rrbracket & = & \nu(x)({\nu_\eta}\llbracket{{\alpha'(t_0, \eta)}}\rrbracket, \ldots, {\nu_\eta}\llbracket{{\alpha'(t_{n - 1}, \eta)}}\rrbracket) \\ & = & \nu(x)({\nu}\llbracket{{t_0}}\rrbracket, \ldots, {\nu}\llbracket{{t_{n-1}}}\rrbracket) \\ & = & {\nu}\llbracket{t}\rrbracket \end{array}$
- If $\eta$ is deﬁned at $x$ then $n = 0$ and $t' = \alpha'(t, \eta) =\, \uparrow\hspace{-0.15em}{{\eta(x)}}$ . Thus ${\nu_\eta}\llbracket{{t'}}\rrbracket = \nu_\eta(\uparrow\hspace{-0.15em}{{\eta(x)}}) = \nu(x) = {\nu}\llbracket{t}\rrbracket$
Assume $t = (a\,x_0 \ldots x_{m-1}.\, t_0 \ldots t_{n-1})$ , and that the shape of $a$ is $(m; {p_0, \ldots, p_{n-1}})$ . Then ${\nu}\llbracket{t}\rrbracket = I'(a)(f_0, \ldots, f_{n-1})$ , where $f_i(u_0, \ldots, u_{m-1}) = {\nu[\overline{x_{p_i} \coloneqq u_{p_i}}]}\llbracket{{t_i}}\rrbracket$ Here $I'$ denotes the same interpretation modiﬁcation as before →.

On the other hand, $t' = \alpha'(t, \eta) = (a\, t'_0 \ldots t'_{n-1})$ , where $t'_i = \alpha'(t_i, (\eta + m)[\overline{x_{p_i} \coloneqq p_i}])$ Then ${\nu_\eta}\llbracket{{t'}}\rrbracket = {\nu_\eta}\llbracket{{(a\, t'_0 \ldots t'_{n-1})}}\rrbracket = I'(a)(f'_0, \ldots, f'_{n-1})$ where $f'_i(u_0, \ldots, u_{n-1}) =\, {\uparrow^{m}\hspace{-0.15em}({\nu_\eta})[\uparrow\hspace{-0.15em}{{0}} \coloneqq u_0, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq u_{m-1}]}\llbracket{{t'_i}}\rrbracket$ It remains to show that $f_i = f'_i$ holds for all $i \in {\overline{n}}$ .

Let $\xi = (\eta + m)[\overline{x_{p_i} \coloneqq p_i}]$ . Clearly, $\xi$ is injective. Then ${\mu_\xi}\llbracket{{t'_i}}\rrbracket = {\mu_\xi}\llbracket{{\alpha'(t_i, \xi)}}\rrbracket = {\mu}\llbracket{{t_i}}\rrbracket$ holds for any valuation $\mu : {{X} \rightarrow U}$ , in particular $\mu = \nu[\overline{x_{p_i} \coloneqq u_{p_i}}]$ . Thus $\begin{array}{rcl} f_i({u_0, \ldots, u_{n-1}}) & = & {\nu[\overline{x_{p_i} \coloneqq u_{p_i}}]}\llbracket{{t_i}}\rrbracket \\ & = & {\nu[\overline{x_{p_i} \coloneqq u_{p_i}}]_\xi}\llbracket{{t'_i}}\rrbracket\\ & = & {\uparrow^{m}\hspace{-0.15em}({\nu_\eta})[\uparrow\hspace{-0.15em}{{0}} \coloneqq u_0, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq u_{m-1}]}\llbracket{{t'_i}}\rrbracket\\ & = & f'_i({u_0, \ldots, u_{n-1}}) \end{array}$ if we can show $L(q) = R(q)$ for all $q \in {\operatorname{FreeAtoms}({t'_i})}$ , where $\begin{array}{rcl} L & = & \nu[\overline{x_{p_i} \coloneqq u_{p_i}}]_\xi \\[0.5em] \text{and}\quad R & = & \, \uparrow^{m}\hspace{-0.15em}({\nu_\eta})[\uparrow\hspace{-0.15em}{{0}} \coloneqq u_0, \ldots, \uparrow\hspace{-0.15em}{{(m-1)}} \coloneqq u_{m-1}] \end{array}$

We show this by case distinction:
- Assume $x \in X$ . We can furthermore assume $x \neq x_k$ for all $k \in p_i$ , because $x_k \notin {\operatorname{FreeAtoms}({t'_i})}$ . Then $L(x) = \nu(x) = R(x)$ .
- Assume $i \in {\overline{{m}}}$ . We can assume $i \in p_i$ , because otherwise $\uparrow\hspace{-0.15em}{i} \notin {\operatorname{FreeAtoms}({t'_i})}$ . Then $L(\uparrow\hspace{-0.15em}{i}) = \nu[\overline{x_{p_i} \coloneqq u_{p_i}}](x)$ where $\xi(x) = i$ , which implies $x = x_i$ . Thus $L(\uparrow\hspace{-0.15em}{i}) = \nu[\overline{x_{p_i} \coloneqq u_{p_i}}](x_i) = u_i = R(\uparrow\hspace{-0.15em}{i})$ .
- Assume $i \in \mathbb{N} \setminus {\overline{{m}}}$ . Then $L(\uparrow\hspace{-0.15em}{i}) = \nu[\overline{x_{p_i} \coloneqq u_{p_i}}](x)$ where $\xi(x) = i$ , which implies $(\eta + m)(x) = i$ , and thus $\eta(x) = i - m$ and $x \neq x_k$ for all $k \in p_i$ . Thus $L(\uparrow\hspace{-0.15em}{i}) = \nu(x)$ where $\eta(x) = i - m$ . On the other hand, $R(\uparrow\hspace{-0.15em}{i}) =\, \uparrow^{m}\hspace{-0.15em}({\nu_\eta})(\uparrow\hspace{-0.15em}{i}) = \nu_\eta(\uparrow\hspace{-0.15em}{(}i - m)) = \nu(y)$ where $\eta(y) = i - m$ . From the injectivity of $\eta$ it follows that $L(\uparrow\hspace{-0.15em}{i}) = \nu(y) = R(\uparrow\hspace{-0.15em}{i})$ .

In particular, for

t \in {\mathcal{T}_{{X}}({\mathfrak{S}})}

and

\nu \in {\includegraphics[height=0.5em]{68F70D64-B406-49B7-864E-B5C7DAC3FF3D}}({X}, U)

{\nu}\llbracket{{\alpha(t)}}\rrbracket = {\nu}\llbracket{t}\rrbracket

An immediate consequence is that

\alpha

-equivalence implies semantical equivalence: Let

s

and

t

\alpha

-equivalent terms in

{\mathcal{T}_{{X}}({\mathfrak{S}})}

, i.e.

\alpha(s) = \alpha(t)

. Then for all valuations

\nu \in {\includegraphics[height=0.5em]{75166EFF-162F-4514-BE94-E38A75FB4F02}}({X}, U)

, we have

{\nu}\llbracket{s}\rrbracket = {\nu}\llbracket{{\alpha(s)}}\rrbracket = {\nu}\llbracket{{\alpha(t)}}\rrbracket = {\nu}\llbracket{t}\rrbracket

Substitution

Before showing that semantical equivalence implies

\alpha

-equivalence in the next section →, we will ﬁrst consider how to perform substitution of (some of) the free atoms in a de Bruijn term.

A substitution is a function

\sigma : {{D} \rightarrow {{\mathcal{B}_{{X}}({\mathfrak{S}})}}}

with domain

D \subseteq X\, \cup \uparrow\hspace{-0.15em}{{\mathbb{N}}}

. Application

t / {\sigma}

of a substitution

\sigma : {{D} \rightarrow {{\mathcal{B}_{{X}}({\mathfrak{S}})}}}

to a de Bruijn term

t \in {\mathcal{B}_{{X}}({\mathfrak{S}})}

is recursively deﬁned as follows:

\begin{array}{rcll} {\uparrow\hspace{-0.15em}{n}} / {\sigma} & = & \sigma(\uparrow\hspace{-0.15em}{n}) \\ & & \text{if}\ \uparrow\hspace{-0.15em}{n}\ \text{is in the domain of}\ \sigma \\[0.5em] {\uparrow\hspace{-0.15em}{n}} / {\sigma} & = & \uparrow\hspace{-0.15em}{n} \\ & & \text{if}\ \uparrow\hspace{-0.15em}{n}\ \text{is not in the domain of}\ \sigma \\[0.5em] {x[{t_0, \ldots, t_{n-1}}]} / {\sigma} & = & ({\sigma(x)} / {\emptyset[\uparrow\hspace{-0.15em}{0} \coloneqq t'_0, \ldots, \uparrow\hspace{-0.15em}{{(n-1)}} \coloneqq t'_{n-1}]}) - n \\ & & \text{if}\ x\ \text{is in the domain of}\ \sigma;\\ & & \text{here}\ \emptyset\ \text{denotes the empty substitution}, \\ & & \text{and}\ t'_i = ({t_i} / {\sigma}) + n \\[0.5em] {x[{t_0, \ldots, t_{n-1}}]} / {\sigma} & = & x[{t_0} / {\sigma}, \ldots, {t_{n-1}} / {\sigma}] \\ & & \text{if}\ x\ \text{is not in the domain of}\ \sigma \\[0.5em] {(a\, t_0 \ldots t_{n-1})} / {\sigma} & = & (a\, t'_0 \ldots t'_{n-1})\ \text{where}\ t'_i =\, {t_i} / {\uparrow^{m}\hspace{-0.15em}({\sigma})},\\ & & \text{given the valence of}\ a\ \text{is}\ m \end{array}

In the above deﬁnition we used the expression

t + z

for

t \in {\mathcal{B}_{{X}}({\mathfrak{S}})}

and

z \in \mathbb{Z}

. This expression is only deﬁned if for all

\uparrow\hspace{-0.15em}{n} \in {\operatorname{FreeAtoms}(t)}

, we have

n + z \geq 0

. Then:

\begin{array}{rcll} t + z & = & t +_0 z &\\ \uparrow\hspace{-0.15em}{n} +_l z & = & \uparrow\hspace{-0.15em}{n} & \text{if}\ n < l \\ \uparrow\hspace{-0.15em}{n} +_l z & = & \uparrow\hspace{-0.15em}{{(n + z)}} & \text{if}\ n \geq l \\ x[{t_0, \ldots, t_{n-1}}] +_l z & = & x[t_0 +_l z, \ldots, t_{n-1} +_l z] \\ (a\, t_0 \ldots t_{n-1}) +_l z & = & (a\, (t_0 +_{l + m} z) \ldots (t_{n-1} +_{l + m} z)) \\ & & \text{where the valence of}\ a\ \text{is}\ m \end{array}

Furthermore, we deﬁne

\uparrow^{m}\hspace{-0.15em}({\sigma})

for a substitution

\sigma : {{D} \rightarrow {{\mathcal{B}_{{X}}({\mathfrak{S}})}}}

and

m \in \mathbb{N}

\begin{array}{rcll} \uparrow^{m}\hspace{-0.15em}({\sigma}) (x) & = & \sigma(x) +_{{x_{\operatorname{arity}}}} m & \text{for}\ x \in X \cap D \\ \uparrow^{m}\hspace{-0.15em}({\sigma}) (\uparrow\hspace{-0.15em}{{(m + n)}}) & = & \sigma(\uparrow\hspace{-0.15em}{n}) + m & \text{for} \uparrow\hspace{-0.15em}{n} \in D \end{array}

Then

\uparrow^{m}\hspace{-0.15em}({\sigma})

is a substitution with domain

(X \cap D) \cup \{\uparrow\hspace{-0.15em}{{(m + n)}} \mid\, \uparrow\hspace{-0.15em}{n} \in D\}

We deﬁne the free atoms of a substitution

\sigma : {{D} \rightarrow {{\mathcal{B}_{{X}}({\mathfrak{S}})}}}

\begin{array}{rcl} {\operatorname{FreeAtoms}({\sigma})} & = & \bigcup_{\uparrow n \in D} {\operatorname{FreeAtoms}({\sigma(\uparrow\hspace{-0.15em}{n})})} \\ & \cup & \bigcup_{x \in D \cap X} \{q - {{x}_{\operatorname{arity}}} \mid q \in {\operatorname{FreeAtoms}({\sigma(x)})} \setminus {\overline{{{{x}_{\operatorname{arity}}}}}})\} \end{array}

We call a substitution

\sigma : {D \rightarrow {{\mathcal{B}_{{X}}({\mathfrak{S}})}}}

regular if

{\operatorname{FreeAtoms}({\sigma})} \subseteq X

For regular

\sigma

we have

\sigma(x) \in {\mathcal{B}_{{X}}^{{{x_{\operatorname{arity}}}}}({\mathfrak{S}})}

for all

x \in D \cap X

and

\sigma(\uparrow\hspace{-0.15em}{n}) \in {\mathcal{B}_{{X}}^{0}({\mathfrak{S}})}

for all

\uparrow\hspace{-0.15em}{n} \in D

Note that if

\sigma

is regular, then

\uparrow^{m}\hspace{-0.15em}({\sigma})

is regular, too.

Given a de Bruijn valuation

\nu

F

U

, any regular substitution

\sigma : {{D} \rightarrow {{\mathcal{B}_{{X}}({\mathfrak{S}})}}}

with

{\operatorname{FreeAtoms}({\sigma})} \subseteq F

induces a de Bruijn valuation

\nu_\sigma

F \cup D

U

via

\begin{array}{rcl} \nu_\sigma(q) & = & \nu(q) \\ & & \text{if}\ q \in F \setminus D \\[0.5em] \nu_\sigma(\uparrow\hspace{-0.15em}{n}) & = & {\nu}\llbracket{{\sigma(\uparrow\hspace{-0.15em}{n})}}\rrbracket\\ & & \text{if}\ \uparrow\hspace{-0.15em}{n} \in D \\[0.5em] \nu_\sigma(x) & = & {\nu}\llbracket{{\sigma(x)}}\rrbracket\\ & & \text{if}\ x \in D \cap X_0 \\[0.5em] \nu_\sigma(x) & = & ({u_0, \ldots, u_{n-1}}) \mapsto\, {\nu[\uparrow\hspace{-0.15em}{0} \coloneqq u_0, \ldots, \uparrow\hspace{-0.15em}{{(n-1)}} \coloneqq u_{n-1}]}\llbracket{{\sigma(x)}}\rrbracket \\ & & \text{if}\ x \in D \cap X \ \text{and where}\ {x_{\operatorname{arity}}} = n > 0 \end{array} <

Abstraction Logic

Introduction

Preliminaries

Algebra

Syntax

Semantics

De Bruijn Terms

α\alphaα-Equivalence

Substitution

$\alpha$ -Equivalence