# On Statman's Finite Completeness Theorem

Richard Statman, Gilles Dowek

► To cite this version:

Richard Statman, Gilles Dowek. On Statman's Finite Completeness Theorem. 2023. [https://inria.hal.science/hal-04198324v1](https://inria.hal.science/hal-04198324v1)

HAL Id: hal-04198324

[https://inria.hal.science/hal-04198324v1](https://inria.hal.science/hal-04198324v1)

Preprint submitted on 7 Sep 2023

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
# On Statman's Finite Completeness Theorem

Richard Statman Gilles Dowek

June 1, 1992

## Abstract

We give a complete self-contained proof of Statman's finite completeness theorem and of a corollary of this theorem stating that the $\lambda$-definability conjecture implies the higher-order matching conjecture.

The purpose of this note is to give a complete self-contained proof of Statman's finite completeness theorem and of a corollary of this theorem stating that the $\lambda$-definability conjecture implies the higher-order matching conjecture. Both results are proved in [8] (theorem 2 and 5). Although, since [8] assumes some familiarity with typed $\lambda$-calculus model theory and presents several results in short space, it may be not very accessible to readers not familiar with this subject.

Section 1 gives the basic notations used in the paper. The reader not familiar with simply typed $\lambda$-calculus should consult Hindley and Seldin [3]. Section 2 presents standard models for simply typed $\lambda$-calculus, it is based on Henkin [2]. Section 3 presents the Completeness theorem, it is based on Friedman [1], Plotkin [5] [6] and Statman [9]. Section 4 presents the construction of a model for some equational theories. Section 5 presents Statman's finite completeness theorem. Both section 4 and 5 are based on [8]. Section 6 presents the $\lambda$-definability conjecture. The notion of $\lambda$-definability is taken from Plotkin [5] [6]. This conjecture has been studied by Plotkin and Statman. At last section 7 presents the higher order matching conjecture and the proof that the $\lambda$-definability conjecture implies the higher order matching conjecture. The decidability of higher order matching is conjectured in Huet [4], the equivalence of the higher order matching problem and the higher order matching problem with closed terms if proved in [7]
and the proof that the λ-definability conjecture implies the higher order matching conjecture is from [8], this proof is also discussed in Wolfram [10].

# 1 Typed λ-calculus

## 1.1 Types

The set of types is defined by

$$T = \iota \mid (T \to T)$$

The notation $\alpha \to \beta \to \gamma$ is an abbreviation for $(\alpha \to (\beta \to \gamma))$.

Obviously a type can be written in a unique way $\alpha = \beta_1 \to \dots \to \beta_n \to \iota$.

If $\alpha$ is a type, the order of $\alpha$ ($o(\alpha)$) is inductively defined by

$$o(\iota) = 1$$

and

$$o(\alpha \to \beta) = \max\{1 + o(\alpha), o(\beta)\}$$

## 1.2 Terms

A context is a set of pairs $\Gamma = \{<x_i, \alpha_i>\}$ where $x_i$ is a variable and $\alpha_i$ is a type, such that if $<x, \alpha> \in \Gamma$ and $<x, \beta> \in \Gamma$ then $\alpha = \beta$.

The set of terms is defined by

$$t = x \mid (t \mid t) \mid \lambda x : T.t$$

The notation $(t \mid u \mid v)$ is an abbreviation for $((t \mid u) \mid v)$.

The judgement the term $t$ has type $\alpha$ in the context $\Gamma$ ($\Gamma \vdash t : \alpha$) is inductively defined by

* if $<x, \alpha> \in \Gamma$ then $\Gamma \vdash x : \alpha$,

* if $\Gamma \vdash t : \alpha \to \beta$ and $\Gamma \vdash u : \alpha$ then $\Gamma \vdash (t \mid u) : \beta$,

* if $\Gamma \cup \{x : \alpha\} \vdash t : \beta$ then $\Gamma \vdash \lambda x : \alpha.t : \alpha \to \beta$.

Obviously if a term $t$ has type $\alpha$ and $\beta$ in a context $\Gamma$ then $\alpha = \beta$.

We write $\Lambda_{\alpha}^{\Gamma}$ for the set of terms $t$ such that $\Gamma \vdash t : \alpha$.
## 1.3 Normalization

If $t$ and $u$ are terms, we write $t[x \leftarrow u]$ for the term obtained by substituting the free occurrences of $x$ by $u$. We write $t \triangleright u$ when $t$, $\beta\eta$-reduces in some steps to $u$. A term is said to be $\beta\eta$-normal if it does not contain any redexes. We write $t =_{\beta\eta} u$ when $t$ and $u$ are $\beta\eta$-equivalent. As proved in [3] the reduction relation is strongly normalizable and confluent on well-typed terms, thus a well-typed term has a unique $\beta\eta$-normal form.

Obviously a normal term can be written in a unique way

$$t = \lambda x_1 : \alpha_1 \dots \lambda x_n : \alpha_n . (x \ c_1 \ \dots \ c_p)$$

where $x$ is a variable.

Let

$$t = \lambda x_1 : \alpha_1 \dots \lambda x_n : \alpha_n . (x \ c_1 \ \dots \ c_p)$$

a normal term of type $\alpha_1 \to \dots \to \alpha_m \to \iota$. The normal $\eta$-long form of $t$ is inductively defined as

$$t' = \lambda x_1 : \alpha_1 \dots \lambda x_n : \alpha_n . \lambda x_{n+1} : \alpha_{n+1} \dots \lambda x_m : \alpha_m . (x \ c'_1 \ \dots \ c'_p \ x'_{n+1} \ \dots \ x'_m)$$

where $c'_i$ is the normal $\eta$-long form of $c_i$ and $x'_j$ is the normal $\eta$-long form of $x_j$.

# 2 Standard Models

In typed $\lambda$-calculus model theory, we do not look at $\lambda$-terms as at functions but rather as at notations for set-theoretical functions.

**Definition: Standard Model**

A *standard model* is a family of sets indexed by types $(M_\alpha)_\alpha$ such that $M_{\alpha \to \beta} = M_\beta^{M_\alpha}$.

**Definition: Assignment**

Let $\Gamma$ be a context $(M_\alpha)_\alpha$ be a standard model, an *assignment from* $\Gamma$ *onto* $(M_\alpha)_\alpha$ is a function $\nu$ which maps every variable $x$ of type $\alpha$ of $\Gamma$ to an element of $M_\alpha$.

**Definition: Interpretation**

Let $\Gamma$ be a context, $(M_\alpha)_\alpha$ be a standard model and $\nu$ an assignment from this context onto this model, we define the function $\tilde{\nu}$ which maps every term of $\Lambda_\alpha^\Gamma$ to an element of $M_\alpha$ by
• $\tilde{\nu}(x) = \nu(x)$,

• if $u$ is a term of type $\alpha \rightarrow \beta$ and $v$ of type $\alpha$ then $\tilde{\nu}(u v) = \tilde{\nu}(u)(\tilde{\nu}(v)),$

• if $u$ is a term of type $\beta$ then for all $d \in M_\alpha$, $\tilde{\nu}(\lambda x : \alpha.u)(d) = \tilde{\nu}^+(u)$ where $\nu^+(x) = d$ and $\nu^+(y) = \nu(y)$ for $y \neq x$.

**Notation:** Let $(M_\alpha)_\alpha$ be a standard model and $t$ and $u$ two terms with the same type $\alpha$, we write $(M_\alpha)_\alpha \models t = u$ if for each assignment $\nu$, we have $\tilde{\nu}(t) = \tilde{\nu}(u)$.

**Remark:** Given a set $M$, there exists only one standard model, $(M_\alpha)_\alpha$ such that $M_\iota = M$.

Moreover if $M$ and $M'$ are two sets with the same cardinal, then we can construct an obvious isomorphism between the standard models $(M_\alpha)_\alpha$ and $(M'_\alpha)_\alpha$ based on $M$ and $M'$. Indeed let us consider a bijection $\Phi$ between $M$ and $M'$ we construct a family of bijections $\Phi_\alpha$ between $M_\alpha$ and $M'_\alpha$ by $\Phi_\iota = \Phi$ and $\Phi_{\alpha \rightarrow \beta}(f) = \Phi_\beta \circ f \circ \Phi_\alpha^{-1}$.

Obviously if $\nu$ is an assignment onto $(M_\alpha)_\alpha$ then the function $\nu'$ which maps every variable $x$ of type $\alpha$ to the element $\Phi_\alpha(\nu(x))$ is an assignment onto $(M'_\alpha)_\alpha$ and for each every $t$ of type $\alpha \tilde{\nu}'(t) = \Phi_\alpha(\tilde{\nu}(t))$. So if $t$ and $u$ are two terms of the same type then $(M_\alpha)_\alpha \models t = u$ if and only if $(M'_\alpha)_\alpha \models t = u$.

So given a cardinal $\xi$ there exists only one standard model (up to isomorphism) such that $M_\iota$ has cardinal $\xi$, we write it $M_\xi$.

# 3 Completeness Theorem

**Definition:** Friedman-Plotkin Model

Assume $\Gamma$ contains an infinite number of variables of each type. Let $M_\iota = \Lambda_\Gamma / =_{\beta\eta}$ and $(M_\alpha)_\alpha$ the standard model built on this set.

**Proposition:** There exists an assignment $\nu$ such that for every $t$ of type $\iota$ we have $\tilde{\nu}(t) = t / =_{\beta\eta}$.

**Proof:** We construct the assignment $\nu$ by induction over the order of the types of the variables of $\Gamma$. If $x$ has type $\iota$ then $\nu(x) = x / =_{\beta\eta}$. Then assume the definition of $\nu(x)$ given for all the variables $x$ of order strictly lower to $k$. Let $\beta = \gamma_1 \rightarrow \dots \rightarrow \gamma_n \rightarrow \iota$ be a type of order lower or equal to $k$, $t$ a term of type $\beta$ and $d \in M_\beta$, we write $t \preceq d$
if for all variables $x_1 : \gamma_1, ..., x_n : \gamma_n$ which do not occur free in $t$ we
have $(t x_1 ... x_n) \in d(\nu(x_1))...(\nu(x_n))$. Obviously if $t \in \tilde{d}$ and $u \in \tilde{d}$
then $t =_{\beta\eta} u$.

Let $x$ be a variable of type $\alpha = \beta_1 \to \dots \to \beta_n \to \iota$ of order $k$, we
define $\nu(x)$ by

$$
\nu(x)(d_1)\dots(d_n) = (x \ t_1 \ \dots \ t_n) / =_{\beta\eta}
$$

if there exists $t_1 \tilde{=} d_1, \dots, t_n \tilde{=} d_n$ (obviously the element $(x t_1 \dots t_n) / =_{\beta\eta}$ does not depend of the choice of $t_1, \dots, t_n$) and $\nu(x)(d_1)\dots(d_n)$ be anything otherwise.

We prove by induction on the structure of the normal $\eta$-long form
of $t$ that $t \in \tilde{\nu}(t)$. Let $t$ be a term of type $\beta_1 \to \dots \to \beta_n \to \iota$. Since
there is in $\Gamma$ an infinite number of variables of each type there are in
$\Gamma$ variables $x_1 : \beta_1, \dots, x_n : \beta_n$ which do not occur free in $t$. Modulo
bound variable renaming the term $t$ can be written

$$
t = \lambda x_1 : \beta_1 \dots \lambda x_n : \beta_n (x \ u_1 \ \dots \ u_p)
$$

By induction hypothesis, for every $i$, we have

$u_i \in \tilde{\nu}(u_i)$

so by definition of $\nu$ we have

$$
\nu(x)(\tilde{\nu}(u_1))...(\tilde{\nu}(u_p)) = (x \ u_1 \ \dots \ u_n) / =_{\beta\eta}
$$

i.e.

$$
(x \ u_1 \ \dots \ u_n) \in \nu(x)(\tilde{\nu}(u_1)) \dots (\tilde{\nu}(u_p))
$$

i.e.

$$
(x \ u_1 \ \dots \ u_n) \in \tilde{\nu}(x \ u_1 \ \dots \ u_p)
$$

so

$$
(\lambda x_1 : \beta_1 \dots \lambda x_n : \beta_n . (x \ u_1 \ \dots \ u_p) \ x_1 \ \dots \ x_n) \\
\in \tilde{\nu} (\lambda x_1 : \beta_1 \dots \lambda x_n : \beta_n . (x \ u_1 \ \dots \ u_p)) (\nu(x_1) \ \dots \ \nu(x_n))
$$

i.e.

$$
(t \ x_1 \ \dots \ x_n) \in \tilde{\nu}(t)(\nu(x_1)) \dots (\nu(x_n))
$$

so

$t \in \tilde{\nu}(t)$

So if $t$ has type $\iota$ then $t \in \tilde{\nu}(t)$, i.e. $\tilde{\nu}(t) = t / =_{\beta\eta}$.
**Theorem:** (Friedman-Plotkin) Completeness Theorem

If $t$ and $u$ are terms of type $\alpha$ then $(M_\alpha)_\alpha \models t = u$ if and only if $t =_{\beta\eta} u$.

**Proof:** Obviously, if $t =_{\beta\eta} u$ then $(M_\alpha)_\alpha \models t = u$. Conversely, if we have $(M_\alpha)_\alpha \models t = u$ then let us write the type of $t$ and $u$ $\alpha = \beta_1 \rightarrow \dots \rightarrow \beta_n \rightarrow \iota$. Since there is in $\Gamma$ an infinite number of variables of each type, there are in $\Gamma$ variables $x_1 : \beta_1, \dots, x_n : \beta_n$ which do not occur free in $t$ and $u$. We have

$$(M_\alpha)_\alpha \models (t x_1 \dots x_n) = (u x_1 \dots x_n)$$

so using the previous proposition

$$(t x_1 \dots x_n) / =_{\beta\eta} = (u x_1 \dots x_n) / =_{\beta\eta}$$

i.e.

$$(t x_1 \dots x_n) =_{\beta\eta} (u x_1 \dots x_n)$$

thus

$$t =_{\beta\eta} u$$

**Corollary:** Let $t$ and $u$ be two terms of type $\alpha$, $t =_{\beta\eta} u$ if and only if for all standard models $M$, $M \models t = u$.

**Corollary:** If $\xi$ is an infinite cardinal and $t$ and $u$ are terms of type $\alpha$ then $M_\xi \models t = u$ if and only if $t =_{\beta\eta} u$.

**Proof:** Let us consider a context $\Gamma$ that contains $\xi$ variables in the type $\iota$ and a denumerable number of variables in the other types. The model $M$ constructed above is such that $M \models t = u$ if and only if $t =_{\beta\eta} u$. This model is isomorphic to the model $M_\xi$ so $M_\xi \models t = u$ if and only if $t =_{\beta\eta} u$.

**Remark:** If $n$ in a finite cardinal then the completeness theorem fails for the model $M_n$ because if $M_\iota$ is finite then $M_\alpha$ is finite for every type $\alpha$ and if $(M_\alpha)_\alpha$ verifies the completeness theorem then $M_{\iota \rightarrow (\iota \rightarrow \iota) \rightarrow \iota}$ is infinite. Indeed call

$$\bar{p} = \lambda x : \iota. \lambda f : \iota \rightarrow \iota. (f \dots (f x) \dots)$$

if $p$ and $q$ are distinct integers then $\bar{p} \neq_{\beta\eta} \bar{q}$ and so $\tilde{\nu}(\bar{p}) \neq \tilde{\nu}(\bar{q})$ and $M_{\iota \rightarrow (\iota \rightarrow \iota) \rightarrow \iota}$ is infinite.

So $M_\xi$ verifies the completeness theorem if and only if $\xi$ is infinite.
# 4 Equational Theories

Let $\Gamma$ be a context such that all the types of the variables in $\Gamma$ are of order at most two. Let $E$ be a set of equations $\{a_i = b_i\}$ where $a_i$ and $b_i$ are well-typed in $\Gamma$ and have type $\iota$ in $\Gamma$. We consider the smallest equivalence relation compatible with term structure that contains $=_{\beta\eta}$ and the equations of $E$. We write this relation $=_{\beta\eta E}$.

**Definition:** The relation $=_{\beta\eta E}$

The relation $=_{\beta\eta E}$ is inductively defined by:

* if $t =_{\beta\eta} u$ then $t =_{\beta\eta E} u$,

* if $a = b \in E$ and $c$ is a term of type $\iota \to \alpha$ then $(c a) =_{\beta\eta E} (c b)$,

* if $t =_{\beta\eta E} u$ then $u =_{\beta\eta E} t$,

* if $t =_{\beta\eta E} u$ and $u =_{\beta\eta E} v$ then $t =_{\beta\eta E} v$,

**Definition:** Statman's Model

Let $M_\iota = \Lambda_\iota^\Gamma / =_{\beta\eta E}$. Let $(M_\alpha)_\alpha$ be the standard model built on $M_\iota$.

**Proposition:** If $(M_\alpha)_\alpha \models t = u$ then $t =_{\beta\eta E} u$.

**Proof:** Let the assignment $\nu$ be defined as

* if $x$ has type $\iota$, then $\nu(x) = x / =_{\beta\eta E}$,

* if $x$ has type $\iota \to \dots \to \iota \to \iota$ then $\nu(x) = f$ where

$$f(d_1)...(d_n) = (x u_1 ... u_n) / =_{\beta\eta E}$$

with $u_1 \in d_1, \dots, u_n \in d_n$ (obviously the class of the term $(x u_1 \dots u_n)$ does not depend on the choice of $u_1, \dots, u_n$).

By induction over the structure of the normal form of $t$, we have for every term $t$ of type $\iota$, $\tilde{\nu}(t) = t / =_{\beta\eta E}$. Indeed, because $t$ has type $\iota$ its normal form can be written $t = (x u_1 \dots u_n)$ since $t$ is well-typed in $\Gamma$ the variable $x$ is of order at most two and the $u_i$ have type $\iota$. So $\tilde{\nu}(u_1) = u_1 / =_{\beta\eta E}, \dots, \tilde{\nu}(u_n) = u_n / =_{\beta\eta E}$. And by definition of $\nu$, $\nu(x)$ maps $u_1 / =_{\beta\eta E}, \dots, u_n / =_{\beta\eta E}$ to $(x u_1 \dots u_n) / =_{\beta\eta E}$. So $\tilde{\nu}(x u_1 \dots u_n) = (x u_1 \dots u_n) / =_{\beta\eta E}$.

If $(M_\alpha)_\alpha \models t = u$ then $\tilde{\nu}(t) = \tilde{\nu}(u)$ so $t / =_{\beta\eta E} = u / =_{\beta\eta E}$ i.e. $t =_{\beta\eta E} u$.
**Remark:** The converse is obviously false. If $E$ contains an equation $x = y$ where $x$ and $y$ are two variables of type $\iota$ and $M$ is a non trivial model then there exists an assignment $\nu$ such that $\nu(x) \neq \nu(y)$.

**Remark:** The proposition is obviously false if $t$ and $u$ do not have type $\iota$. Indeed consider a variable $f$ of type $\iota \to \iota$ and a set $E$ which contains the equations $(f t) = t$ for all the terms $t$ of type $\iota$, we have $M \models f = \lambda x : \iota.x$ but $f \neq_{\beta\eta E} \lambda x : \iota.x$.

**Remark:** The proposition is obviously false if $\Gamma$ contains variables of order greater than two. Indeed consider a variable $f$ of type $\iota \to \iota$ and $F$ of type $(\iota \to \iota) \to \iota$ and a set $E$ which contains the equations $(f t) = t$ for all the terms $t$ of type $\iota$, we have $M \models (F f) = (F \lambda x : \iota.x)$ but $(F f) \neq_{\beta\eta E} (F \lambda x : \iota.x)$.

# 5 Finite Models

**Definition:** A model is said to be *finite* if the set $M_\iota$ is finite.

We want to sharpen the completeness theorem of section 3 and build a finite model. As remarked in section 3, the completeness theorem fails for such a model, so our completeness requirement will be weaker. For each closed term $t$, we are going to construct a finite model $M_t$ such that for each closed term $u$, $M_t \models t = u$ if and only if $t =_{\beta\eta} u$. We do not require the model $M_t$ to be uniform over $t$.

## 5.1 A Remark on the Relation $\equiv_{\beta\eta E}$

**Proposition:** Let $E = \{a_i = b_i\}$ be a set of equations such that for every $i$, $a_i$ and $b_i$ have type $\iota$. Let $t$ and $u$ be two terms such that $t =_{\beta\eta E} u$. Then either the normal forms of $t$ and $u$ are identical or they both have a subterm in the set $T = \{a_i, b_i\}$.

**Proof:** By induction on the structure of the proof of $t =_{\beta\eta E} u$.

* If $t =_{\beta\eta} u$ then the normal forms of $t$ and $u$ are identical.

* If $t = (c a)$ and $u = (c b)$ then if $x$ has an occurrence in the normal form of $(c x)$ then $a$ is a subterm of the normal form of $(c a)$ and $b$ is a subterm of the normal form of $(c b)$. Otherwise the terms $(c a)$ and $(c b)$ have the same normal form.
• if $u =_{\beta\eta E} t$ then by induction hypothesis, either the normal forms of $u$ and $t$ are identical of they both have a subterm in $T$.

• If $t =_{\beta\eta E} v$ and $v =_{\beta\eta E} u$ then call $t'$, $v'$, $u'$ the normal forms of $t$, $v$, $u$. By induction hypothesis, either

- $t' = v'$ and $v' = u'$, in this case $t' = u'$,

- $t'$ and $v'$ have a subterm in $T$ and $v' = u'$, in this case $t'$ and $u'$ have a subterm in $T$,

- $t' = v'$ and $v'$ and $u'$ have a subterm in $T$, in this case $t'$ and $u'$ have a subterm in $T$,

- $t'$ and $v'$ have a subterm in $T$ and $v'$ and $u'$ have a subterm in $T$, in this case $t'$ and $u'$ have a subterm in $T$.

**Corollary:** Let $E = \{a_i = b_i\}$ be a set of equations such that for every $i$, $a_i$ and $b_i$ have type $\iota$. Let $t$ and $u$ be two terms such that no subterm of the normal form of $t$ is an $a_i$ or a $b_i$, then $t =_{\beta\eta E} u$ if and only if $t =_{\beta\eta} u$.

## 5.2 Finite Models for Terms of Order Lower than Three

Before giving the theorem in its full generality, we shall consider the simpler case in which the order of the type of $t$ is lower than three.

**Proposition:** Let $t$ be a closed term which type is of order at most three. There exists a finite model $M_t$ such that $M_t \models t = u$ if and only if $t =_{\beta\eta} u$, and the number of elements of $M_t$ is computable in function of $t$.

**Proof:** Let $\alpha = \beta_1 \rightarrow \dots \rightarrow \beta_n \rightarrow \iota$ be the type of $t$. Let $\Gamma$ be the context $\Gamma = \{x_1 : \beta_1, \dots, x_n : \beta_n\}$. The types of the variables of $\Gamma$ are of order at most two. Let $u$ be a closed term of type $\alpha$, we have $t =_{\beta\eta} u$ if and only if $(t \ x_1 \ \dots \ x_n) =_{\beta\eta} (u \ x_1 \ \dots \ x_n)$. Let $E$ be the set containing all the equations $a = b$ with $a$ and $b$ in $\Lambda_\iota^\Gamma$ and neither $a$ nor $b$ is a subterm of the normal form of $(t \ x_1 \ \dots \ x_n)$. Using the proposition above $(t \ x_1 \ \dots \ x_n) =_{\beta\eta} (u \ x_1 \ \dots \ x_n)$ if and only if $(t \ x_1 \ \dots \ x_n) =_{\beta\eta E} (u \ x_1 \ \dots \ x_n)$.

Let us consider the model $M_t$ constructed at the section 4. Obviously if $t =_{\beta\eta} u$ then $M_t \models t = u$. Conversely if we have $M_t \models t = u$
then $M_t \models (t x_1 \dots x_n) = (u x_1 \dots x_n)$. So $(t x_1 \dots x_n) =_{\beta\eta E} (u x_1 \dots x_n)$, therefore $(t x_1 \dots x_n) =_{\beta\eta} (u x_1 \dots x_n)$ and $t =_{\beta\eta} u$.

The number of elements of $M_\iota$ is $1+k$ where $k$ is the number of distinct subterms of the normal form of $(t x_1 \dots x_n)$ of type $\iota$, it is therefore a computable in function of $t$.

## 5.3 General Case

**Definition: Length of a Term**

Let $t = \lambda x_1 : \alpha_1 \dots \lambda x_n : \alpha_n (x d_1 \dots d_n)$ be a normal $\eta$-long term, we define the length of $t$ ($|t|$) by induction on the number of variables occurrences of $t$ by

$$|t| = 1 + \max\{|\lambda x_1 : \alpha_1 \dots \lambda x_n : \alpha_n . d_i|\}$$

Consider a closed term $t$ of type $\alpha$, we shall prove that we can find terms $w_1, \dots, w_p$ of type $\alpha \to \iota$ which free variables are of order at most two and such that for each closed term $u$ of type $\alpha$, $t =_{\beta\eta} u$ if and only if for all $i$, $(w_i t) =_{\beta\eta} (w_i u)$. Then we will be able to conclude as above.

Without loss of generality, we can assume that $t$ is normal $\eta$-long. We shall first construct a term $w$ such that $(w t) \neq_{\beta\eta} (w u)$ for all the normal $\eta$-long closed terms $u$ that do not have the same length as $t$. Then for each normal $\eta$-long closed term $u$ such that $u \neq t$ and $u$ has the same length as $t$ we shall construct a term $w$ such that $(w t) \neq_{\beta\eta} (w u)$. Since the number of normal $\eta$-long closed terms which have a given length and a given type is finite, this will give us a finite number of $w_i$.

**Proposition:** Let $t$ be a normal $\eta$-long closed term of type $\alpha$, there exists a term $w$ of type $\alpha \to \iota$ such that for every normal $\eta$-long closed term $u$ of type $\alpha$, if $|t| \neq |u|$ then $(w t) \neq_{\beta\eta} (w u)$ and the free variables of $w$ are of order at most two.

**Proof:** For each integer $p$ consider a variable $z_p$ of type $\iota \to \dots \to \iota \to \iota$. We define by induction over the structure of $\alpha$ a term $c_\alpha$. Let us write

$$\alpha = \beta_1 \to \dots \to \beta_p \to \iota$$

and

$$\beta_1 = \gamma_1^1 \to \dots \to \gamma_{q_1}^1 \to \iota$$
...

$$ \beta_p = \gamma_1^p \rightarrow \dots \rightarrow \gamma_{qp}^p \rightarrow \iota $$

Let us define

$$ c_{\alpha} = \lambda x_1 : \beta_1 \dots \lambda x_p : \beta_p (z_p (x_1 c_{\gamma_1^1} \dots c_{\gamma_{q_1}^1}) \dots (x_p c_{\gamma_1^p} \dots c_{\gamma_{qp}^p})) $$

Now consider a term

$$ t = \lambda y_1 : \alpha_1 \dots \lambda y_n : \alpha_n (y_i d_1 \dots d_p) $$

Let us write

$$ \alpha_i = \beta_1 \rightarrow \dots \rightarrow \beta_p \rightarrow \iota $$

and

$$ \beta_1 = \gamma_1^1 \rightarrow \dots \rightarrow \gamma_{q_1}^1 \rightarrow \iota $$

...

$$ \beta_p = \gamma_1^p \rightarrow \dots \rightarrow \gamma_{qp}^p \rightarrow \iota $$

Let us define

$$ e_1 = \lambda y_1 : \alpha_1 \dots \lambda y_n : \alpha_n d_1 $$

...

$$ e_p = \lambda y_1 : \alpha_1 \dots \lambda y_n : \alpha_n d_p $$

We have

$$ (t c_{\alpha_1} \dots c_{\alpha_n}) =_{\beta\eta} (z_p (e_1 c_{\alpha_1} \dots c_{\alpha_n} c_{\gamma_1^1} \dots c_{\gamma_{m_1}^1}) \dots (e_p c_{\alpha_1} \dots c_{\alpha_n} c_{\gamma_1^p} \dots c_{\gamma_{mp}^p})) $$

By induction on the length of $t$, the length of the normal form of the term $(t c_{\alpha_1} \dots c_{\alpha_n})$ is the length of $t$. So if $|t| \neq |u|$ then the length of the normal forms of the terms $(t c_{\alpha_1} \dots c_{\alpha_n})$ and $(u c_{\alpha_1} \dots c_{\alpha_n})$ are different and $(t c_{\alpha_1} \dots c_{\alpha_n}) \neq_{\beta\eta} (u c_{\alpha_1} \dots c_{\alpha_n})$.

We take $w = \lambda x : \alpha.(x c_{\alpha_1} \dots c_{\alpha_n})$. If $|t| \neq |u|$ then $(w t) \neq_{\beta\eta} (w u)$.

**Proposition:** Let $t$ and $u$ be two distinct normal $\eta$-long closed terms of type $\alpha = \alpha_1 \rightarrow \dots \rightarrow \alpha_n \rightarrow \iota$. There are terms $c_1, \dots, c_n$ of type $\alpha_1, \dots, \alpha_n$ such that $(t c_1 \dots c_n) \neq_{\beta\eta} (u c_1 \dots c_n)$ and the free variables of $c_1, \dots, c_n$ are of order at most two.

**Proof:** By induction on the number of variables occurrences of $t$. Let us write

$$ t = \lambda x_1 : \alpha_1 \dots \lambda x_n : \alpha_n (x_i d_1 \dots d_p) $$
and

$$u = \lambda x_1 : \alpha_1 \dots \lambda x_n : \alpha_n (x_{i'} d'_1 \dots d'_{p'})$$

First Case: $i \neq i'$

Let $\alpha_i = \beta_1 \to \dots \to \beta_p \to \iota$ and $\alpha_{i'} = \beta'_1 \to \dots \to \beta'_{p'} \to \iota$. We let $z$ and $z'$ be two new variables of type $\iota$ and we take $c_i = \lambda y_1 : \beta_1 \dots \lambda y_p : \beta_p \cdot z$ and $c_{i'} = \lambda y_1 : \beta'_1 \dots \lambda y'_{p'} : \beta'_{p'} \cdot z'$ and $c_j$ be any term when $j \neq i$ and $j \neq i'$. We have $(t \ c_1 \ \dots \ c_n) =_{\beta\eta} z$ and $(u \ c_1 \ \dots \ c_n) =_{\beta\eta} z'$ so $(t \ c_1 \ \dots \ c_n) \neq_{\beta\eta} (u \ c_1 \ \dots \ c_n)$.

Second Case: $i = i'$

So we have $p = p'$. For all $j$ we let $e_j = \lambda x_1 : \alpha_1 \dots \lambda x_n : \alpha_n \cdot d_j$ and $e'_j = \lambda x_1 : \alpha_1 \dots \lambda x_n : \alpha_n \cdot d'_j$. We have

$$t =_{\beta\eta} \lambda x_1 : \alpha_1 \dots \lambda x_n : \alpha_n (x_i (e_1 x_1 \dots x_n) \dots (e_p x_1 \dots x_n))$$

and

$$u =_{\beta\eta} \lambda x_1 : \alpha_1 \dots \lambda x_n : \alpha_n (x_i (e'_1 x_1 \dots x_n) \dots (e'_p x_1 \dots x_n))$$

Since $t \neq_{\beta\eta} u$ there exists an integer $k$ such that $e_k \neq_{\beta\eta} e'_k$. Let us write $\alpha_i = \beta_1 \to \dots \to \beta_p \to \iota$ and $\beta_k = \gamma_1 \to \dots \to \gamma_m \to \iota$. The type of the terms $e_k$ and $e'_k$ is $\alpha_1 \to \dots \to \alpha_n \to \gamma_1 \to \dots \to \gamma_m \to \iota$. By induction hypothesis there exists terms $a_1, \dots, a_n, b_1, \dots, b_m$ such that

$$(e_k a_1 \dots a_n b_1 \dots b_m) \neq_{\beta\eta} (e'_k a_1 \dots a_n b_1 \dots b_m)$$

We let $z$ be a new variable of type $\iota \to \iota \to \iota$. We let

$$c_i = \lambda y_1 : \beta_1 \dots \lambda y_p : \beta_p (z (y_k b_1 \dots b_m) (a_i y_1 \dots y_p))$$

and $c_j = a_j$ for every $j \neq i$.

Remark that for each $j$, $c_j[z \leftarrow \lambda x : \iota.\lambda y : \iota.y] =_{\beta\eta} a_j$, so

$$(e_k c_1 \dots c_n b_1 \dots b_m) \neq_{\beta\eta} (e'_k c_1 \dots c_n b_1 \dots b_m)$$

otherwise we would have $(e_k a_1 \dots a_n b_1 \dots b_m) =_{\beta\eta} (e'_k a_1 \dots a_n b_1 \dots b_m)$ by substituting the variable $z$ by the term $\lambda x : \iota.\lambda y : \iota.y$. Now

$$(t c_1 \dots c_n) =_{\beta\eta} (z (e_k c_1 \dots c_n b_1 \dots b_m) (a_i (e_1 c_1 \dots c_n) \dots (e_p c_1 \dots c_n)))$$

and

$$(u c_1 \dots c_n) =_{\beta\eta} (z (e'_k c_1 \dots c_n b_1 \dots b_m) (a_i (e'_1 c_1 \dots c_n) \dots (e'_p c_1 \dots c_n)))$$
So

$$ (t c_1 \dots c_n) \neq_{\beta\eta} (u c_1 \dots c_n) $$

**Proposition:** Let $t$ and $u$ be two distinct normal $\eta$-long closed terms of type $\alpha$, there exists a term $w$ of type $\alpha \to \iota$ such that $(w t) \neq_{\beta\eta} (w u)$ and the free variables of $w$ are of order at most two.

**Proof:** Let $\alpha = \alpha_1 \to \dots \to \alpha_n \to \iota$, by the previous proposition there are terms $c_1, \dots, c_n$ such that $(t c_1 \dots c_n) \neq_{\beta\eta} (u c_1 \dots c_n)$, and the free variables of $c_1, \dots, c_n$ are of order at most two. We take $w = \lambda x : \alpha.(x c_1 \dots c_n)$.

**Proposition:** Let $t$ be a closed term of type $\alpha$, there exist terms $w_1, \dots, w_p$ of type $\alpha \to \iota$ which free variables are of order at most two and such that for each term $u$, $t =_{\beta\eta} u$ if and only if for all $i$, $(w_i t) =_{\beta\eta} (w_i u)$.

**Proof:** We construct, using a previous proposition, a term $w$ such that for each normal $\eta$-long closed term $u$ of type $\alpha$ which length is different from the length of the normal $\eta$-long form of $t$, $(w t) \neq_{\beta\eta} (w u)$. Then for each normal $\eta$-long closed term $u$ of type $\alpha$ which has the same length as the normal $\eta$-long form of $t$ and which is different from the normal form of $t$, we construct, using a previous proposition, a term $w$ such that $(w t) \neq_{\beta\eta} (w u)$. Since the number of normal $\eta$-long closed terms which have the same length and the same type as the normal $\eta$-long form of $t$ is finite, this gives us a finite number of $w_i$.

Obviously, for each closed term $u$ of type $\alpha$, $t =_{\beta\eta} u$ if and only if for each integer $i$, $(w_i t) =_{\beta\eta} (w_i u)$.

**Theorem:** (Statman) Finite Completeness Theorem

Let $t$ be a closed term of type $\alpha$. There exists a finite model $M_t$ such that $M_t \models t = u$ if and only if $t =_{\beta\eta} u$, and the number of elements of $M_t$ is computable in function of $t$.

**Proof:** Let $w_1, \dots, w_n$ the terms given by the proposition above. Let $E$ be the set containing all the equations $a = b$ with $a$ and $b$ in $\Lambda_{\iota}^{\Gamma}$ and neither $a$ nor $b$ is a subterm of the normal form of an $(w_i t)$ for some $i$. Using a proposition above $(w_i t) =_{\beta\eta} (w_i u)$ if and only if $(w_i t) =_{\beta\eta E} (w_i u)$.

Let us consider the model $M_t$ constructed at the section 4. Obviously if $t =_{\beta\eta} u$ then we have $M_t \models t = u$. Conversely if $M_t \models t = u$ then $M_t \models (w_i t) = (w_i u)$. So $(w_i t) =_{\beta\eta E} (w_i u)$, therefore $(w_i t) =_{\beta\eta} (w_i u)$ and $t =_{\beta\eta} u$.
The number of elements of $M_t$ is $1 + k$ where $k$ is the number of distinct subterms of the normal form of $(w_i t)$ of type $ι$, since the terms $w_i$ are computable in function of $t$, the number of elements of $M_t$ is computable in function of $t$.

**Corollary:** Let $t$ and $u$ two terms of type $\alpha$, $t =_{\beta\eta} u$ if and only if for all the finite standard models $M, M \models t = u$.

# 6 The $\lambda$-definability Conjecture

Because a simple function as the identity over integers is an infinite set (although it has a finite description), set-theoretical functions are not usually computational objects. In the same way, because completeness theorems concern usually infinite sets, model checking is not usually an effective decision procedure. Both argument fail when the sets involved are finite. Indeed, finite set-theoretical functions are computational objects (e.g. association lists) and finite model checking is an effective decision procedure (e.g. propositional calculus).

**Definition:** Let $(M_\alpha)_\alpha$ be the standard model with the base set $M = M_t$. A function $f$ of $M_\alpha$ is said to be $\lambda$-definable if there exists a closed $\lambda$-term $t$ of type $\alpha$ such that $\tilde{v}(t) = f$ (where $v$ is the only assignment over the empty set).

**Conjecture:** $\lambda$-definability Conjecture

If $M$ is finite then it is decidable whether of not a function $f$ of $M_\alpha$ is $\lambda$-definable.

**Remark:** The problem makes sense because $M$ is finite, otherwise the functions of $M_\alpha$ would not be computational objects.

# 7 The $\lambda$-definability Conjecture Implies the Higher Order Matching Conjecture

**Definition:** Higher Order Matching Problem

A *higher order matching problem* is a pair of terms < *a*, *b* > of types
*α*₁ → ... → *α*ₙ → *β* and *β*. A solution to this problem is a *n*-uple of
terms < *t*₁, ..., *t*ₙ > of type *α*₁, ..., *α*ₙ such that (*a* *t*₁ ... *t*ₙ) = *β*ₗ *b*.
**Conjecture :** Higher Order Matching Conjecture

It is decidable whether of not a higher order matching problem has a solution.

**Proposition:** The higher order matching problem is decidable if and only if the higher order matching problem with closed a and b is decidable.

**Proof:** Let <a, b> be a problem. Let x₁ : β₁, ..., xₚ : βₚ be the free variables occurring in a and b. Let

$$\gamma_1 = \beta_1 \rightarrow \dots \rightarrow \beta_p \rightarrow \alpha_1$$

$$\gamma_n = \beta_1 \rightarrow \dots \rightarrow \beta_p \rightarrow \alpha_n$$

$$a' = \lambda y_1 : \gamma_1 \dots \lambda y_n : \gamma_n . \lambda x_1 : \beta_1 \dots \lambda x_p : \beta_p . (a (y_1 x_1 \dots x_p) \dots (y_n x_1 \dots x_p))$$

$$b' = \lambda x_1 : \beta_1 \dots \lambda x_p : \beta_p . b$$

If we have

$$(a \ t_1 \ \dots \ t_n) = b$$

then

$$(a' \ \lambda x_1 : \beta_1 \dots \lambda x_p : \beta_p . t_1 \ \dots \ \lambda x_1 : \beta_1 \dots \lambda x_p : \beta_p . t_n) = b'$$

Conversely if we have

$$(a' \ t'_1 \ \dots \ t'_n) = b'$$

then

$$(a (t'_1 x_1 \dots x_p) \dots (t'_n x_1 \dots x_p)) = b$$

So the problem <a, b> has a solution if and only if the problem <a', b'> has one.

**Proposition:** The higher order matching problem is decidable if and only if the higher order matching problem with closed t₁, ..., tₙ is decidable.

**Proof:** Let <a, b> be a problem. Let

$$a' = \lambda y_1 : \iota \rightarrow \alpha_1 \dots \lambda y_n : \iota \rightarrow \alpha_n . \lambda x : \iota . (a (y_1 x) \dots (y_n x))$$

and

$$b' = \lambda x : \iota . b$$
(remark that if a and b are closed then a' and b' also are).

Assume the problem < a, b > has a solution $t_1, ..., t_n$. Let $z$ be a variable of type $\iota$. For each type $\beta = \gamma_1 \rightarrow ... \rightarrow \gamma_k \rightarrow \iota$ we consider the term $w_\beta = \lambda z_1 : \gamma_1 ... \lambda z_k : \gamma_k z$.

Let $x_1 : \beta_1, ..., x_p : \beta_p$ be the variables occurring free in the terms $t_1, ..., t_n$, $t'_i = t_i[x_1 \leftarrow w_{\beta_1}, ..., x_k \leftarrow w_{\beta_k}]$ and $u_i = \lambda z : \iota.t'_i$. We have

$$ (a' u_1 ... u_n) = b' $$

So the problem < a', b' > has closed solution.

Now if the problem < a', b' > has a closed solution $u_1, ..., u_n$ then let $z$ be a variable of type $\iota$ and $t_i = (u_i z)$. We have

$$ (a' u_1 ... u_n) = b' $$

so

$$ \lambda x : \iota.(a (u_1 x) ... (u_n x)) = \lambda x : \iota.b $$

so

$$ (a (u_1 z) ... (u_n z)) = b $$

i.e.

$$ (a t_1 ... t_n) = b $$

So the problem < a, b > has a solution if and only if the problem < a', b' > has a closed solution.

**Theorem:** (Statman) If $\lambda$-definability is decidable then higher order matching is decidable.

**Proof:** Let us assume the $\lambda$-definability conjecture. We take two closed terms $a : \alpha_1 \rightarrow ... \alpha_n \rightarrow \beta$ and $b : \beta$ and consider the model $M_b$ constructed in section 5. Let $A = \tilde{\nu}(a)$ and $B = \tilde{\nu}(b)$ (where $\nu$ is the only assignment over the empty set). By an enumeration procedure we select all the n-uples < $T_1, ..., T_n$ > such that $A(T_1, ..., T_n) = B$. The problem < $a, b$ > has a closed solution if and only if there is such a n-uple such that all the $T_i$ are $\lambda$-definable.

Indeed if the problem < $a, b$ > has a closed solution < $t_1, ..., t_n$ >, then let $T_i = \tilde{\nu}(t_i)$, the $T_i$ are $\lambda$-definable and $A(T_1, ..., T_n) = B$. Conversely if there are $\lambda$-definable $T_1, ... T_n$ such that $A(T_1, ..., T_n) = B$. Let $t_1, ..., t_n$ be the terms such that $T_i = \tilde{\nu}(t_i)$. We have $M_b \models (a t_1 ... t_n) = b$. So $(a t_1 ... t_n) =_{\beta\eta} b$.
References

[1] H. Friedman, Equality Between Functionals, *Proceedings of Logical Colloquium 72-73*, Lecture Notes in Mathematics, 453, R. Parikh (Ed.), Springer-Verlag, 1975, pp. 22-37.

[2] L. Henkin, Completeness in the Theory of Types, *Journal of Symbolic Logic*, 15, 2, 1950, pp. 81-91.

[3] J.R. Hindley, J.P. Seldin, Introduction to Combinators and λ-Calculus, *Cambridge University Press*, 1986.

[4] G. Huet, Résolution d'Équations dans les Langages d'Ordre 1,2, ..., ω, *Thèse de Doctorat d'État*, Université de Paris 7, 1976.

[5] G. D. Plotkin, Lambda-definability and Logical Relations, *Memorandum SAI-RM-4*, University of Edinburgh, 1973.

[6] G. D. Plotkin, Lambda-Definability in the Full Type Hierarchy, *To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism*, J.R. Hindley and J.P. Seldin (Eds.), Academic Press, 1980, pp. 365-373.

[7] R. Statman, On the Existence of Closed Terms in the Typed λ-calculus II: Transformations of Unification Problems, *Theoretical Computer Science*, 15, 1981, pp. 329-338.

[8] R. Statman, Completeness, Invariance and λ-definability, *Journal of Symbolic Logic*, 47, 1, 1982, pp. 17-26.

[9] R. Statman, Equality Between Functionals Revisited, *Harvey Friedman's Research on the Foundations of Mathematics*, L. A. Harrington et al. (Ed.), North-Holland, 1985, pp. 331-338.

[10] D. A. Wolfram, The Clausal Theory of Types, *PhD Thesis*, Cambridge University, 1989.