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?

|cite|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 acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Browse other questions tagged or ask your own question.