<p>Let $T$ be the complete hierarchy of functions over $\mathbb{N}$.  That is: $T$ = $\bigcup T_{\tau}$ for all simple types $\tau$ built up from the basic type $\mathbb{N}$, with $T_{\mathbb{N}} = \mathbb{N}$ and $T_{\alpha→\beta} = {T_\beta}^{T_\alpha}$.  For a given signature $\Sigma$ consisting of some members of $T$, there is an obvious way of interpreting the closed terms of type $\tau$ in a simply typed $\lambda$-language $\mathcal{L}_\Sigma$ with constants from $\Sigma$ as denoting functions in $T_\tau$.  Let ${T^\Sigma}$ contain just those members of $T$ that are denoted by closed terms in $\mathcal{L}_\Sigma$.  Say that $T^\Sigma$ is <em>functional</em> just in case, for any distinct $f, g ∈ {T^\Sigma}_{\alpha→\beta}$, there is some $x ∈ {T^\Sigma}_\alpha$ such that $f(x) \ne g(x)$.  </p>

<p>Specific question: let $\Sigma$ consist in all members of $\mathbb{N}$ (of type $\mathbb{N}$) together with the addition function (of type $\mathbb{N}→\mathbb{N}→\mathbb{N}$).  Is this $T^\Sigma$ functional?  </p>

<p>More general question: is there any useful general condition on $\Sigma$ that is sufficient for $T^\Sigma$ to be functional?  </p>

CC BY-SA 3.0
2015-11-18T16:22:38.267Z
Does $T$ range over all functions, including non-computable ones? What do you mean by "simply typed λ-language"?
Martin Berger
CC BY-SA 3.0
2015-11-19T18:14:10.607Z
Yes, T includes all functions.  By a simply typed λ-language, I mean the following.  First we define types: '$\mathbb{N}$' is a type; α→β is a type whenever α and β are; nothing else is a type.   For each type we have an infinite supply of variables of that type.  Then we define terms of a type: a variable of a type is a term of that type; (XY) is a term of type β whenever X is a term of type α→β and Y is a term of type α; (λvX) is a term of type α→β whenever v is a variable of type α and X is a term of type β; nothing else is a term.
Cian
CC BY-SA 3.0
2015-11-19T18:21:48.807Z
A simply typed λ-language with constants from Σ is similar except that now members of Σ are also terms of appropriate type.
Cian
CC BY-SA 3.0
2015-11-20T09:03:33.213Z
Thanks. How about $\Sigma = \{id, succ\}$ where $id$ is the identity function on $\mathbb{N}$ and $succ$ the successor function on $\mathbb{N}$? Since you cannot construct elements of $\mathbb{N}$ from closed terms in this setting, $id$ and $succ$ cannot be distinguished.
Martin Berger
CC BY-SA 3.0
2015-11-21T14:58:14.230Z
Right, so a sufficient condition for $T^Σ$ *not* to be functional is that $Σ$ contains some member of type $\mathbb{N}→\mathbb{N}$ (or $\mathbb{N} →\cdots→\mathbb{N}$) but doesn't contain any members of $\mathbb{N}$---there's no way of "constructing" one if we aren't given any of them to begin with.
Cian
<typed-lambda-calculus><extensionality>
Functionality of a hierarchy of definable functions over $\mathbb{N}$
Cian
# Functionality of a hierarchy of definable functions over $\mathbb{N}$

(Asked by: username_0 on 2015-11-16)

Let $T$ be the complete hierarchy of functions over $\mathbb{N}$. That is: $T$ = $\bigcup T\_{\tau}$ for all simple types $\tau$ built up from the basic type $\mathbb{N}$, with $T\_{\mathbb{N}} = \mathbb{N}$ and $T\_{\alpha→\beta} = {T\_\beta}^{T\_\alpha}$. For a given signature $\Sigma$ consisting of some members of $T$, there is an obvious way of interpreting the closed terms of type $\tau$ in a simply typed $\lambda$-language $\mathcal{L}\_\Sigma$ with constants from $\Sigma$ as denoting functions in $T\_\tau$. Let ${T^\Sigma}$ contain just those members of $T$ that are denoted by closed terms in $\mathcal{L}\_\Sigma$. Say that $T^\Sigma$ is *functional* just in case, for any distinct $f, g ∈ {T^\Sigma}\_{\alpha→\beta}$, there is some $x ∈ {T^\Sigma}\_\alpha$ such that $f(x) \ne g(x)$.

Specific question: let $\Sigma$ consist in all members of $\mathbb{N}$ (of type $\mathbb{N}$) together with the addition function (of type $\mathbb{N}→\mathbb{N}→\mathbb{N}$). Is this $T^\Sigma$ functional?

More general question: is there any useful general condition on $\Sigma$ that is sufficient for $T^\Sigma$ to be functional?

**Tags:** typed-lambda-calculus, extensionality
> **Comments:**
> **username_1**: Does $T$ range over all functions, including non-computable ones? What do you mean by "simply typed λ-language"?  
> **username_0**: Yes, T includes all functions.  By a simply typed λ-language, I mean the following.  First we define types: '$\mathbb{N}$' is a type; α→β is a type whenever α and β are; nothing else is a type.   For each type we have an infinite supply of variables of that type.  Then we define terms of a type: a variable of a type is a term of that type; (XY) is a term of type β whenever X is a term of type α→β and Y is a term of type α; (λvX) is a term of type α→β whenever v is a variable of type α and X is a term of type β; nothing else is a term.  
> **username_0**: A simply typed λ-language with constants from Σ is similar except that now members of Σ are also terms of appropriate type.  
> **username_1**: Thanks. How about $\Sigma = \{id, succ\}$ where $id$ is the identity function on $\mathbb{N}$ and $succ$ the successor function on $\mathbb{N}$? Since you cannot construct elements of $\mathbb{N}$ from closed terms in this setting, $id$ and $succ$ cannot be distinguished.  
> **username_0**: Right, so a sufficient condition for $T^Σ$ *not* to be functional is that $Σ$ contains some member of type $\mathbb{N}→\mathbb{N}$ (or $\mathbb{N} →\cdots→\mathbb{N}$) but doesn't contain any members of $\mathbb{N}$---there's no way of "constructing" one if we aren't given any of them to begin with.  

---

## 0 answers

