3
$\begingroup$

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?

Improve this question
$\endgroup$
  • $\begingroup$ Does $T$ range over all functions, including non-computable ones? What do you mean by "simply typed λ-language"? $\endgroup$ – Martin Berger Nov 18 '15 at 16:22
  • $\begingroup$ 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. $\endgroup$ – Cian Nov 19 '15 at 18:14
  • $\begingroup$ A simply typed λ-language with constants from Σ is similar except that now members of Σ are also terms of appropriate type. $\endgroup$ – Cian Nov 19 '15 at 18:21
  • $\begingroup$ 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. $\endgroup$ – Martin Berger Nov 20 '15 at 9:03
  • $\begingroup$ 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. $\endgroup$ – Cian Nov 21 '15 at 14:58

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.