Skip to main content

All Questions

Filter by
Sorted by
Tagged with
3 votes
0 answers
138 views

When can all elements of $[A\to B]$ can be represented as computable functions?

(crosspost from math stackexchange) While working through Barendreght's book on the Lambda Calculus, and Abramsky's notes on Domain Theory, I had the following realization: It's often stated that ...
Alex Appel's user avatar
8 votes
0 answers
155 views

Is every total computable function definable by a strongly total lambda term?

Every computable (total) function $f : \mathbb{N} \to \mathbb{N}$ is definable in untyped pure lambda calculus in the sense that there is a term $F$ such that, for every Church's numeral $c_n = \...
Valery Isaev's user avatar
  • 4,459
8 votes
1 answer
321 views

Is every total computable function definable by a normalizing lambda term?

$\newcommand{\nat}{\mathbb{N}}$ $\newcommand{\then}{\ \Longrightarrow\ }$ A partial function $f : \mathbb{N} \to \mathbb{N}$ is said to be $\lambda$-definable if there is a term $F \in \Lambda$ such ...
Andrew Polonsky's user avatar
9 votes
2 answers
2k views

Is simply typed lambda calculus with fixed-point combinator Turing-complete?

There are many sources cite that simply typed lambda calculus extended with fixed-point combinator is Turing complete. For example, Does there exist a Turing complete typed lambda calculus? or the ...
kittyphon's user avatar
  • 101
3 votes
2 answers
327 views

Comparing really big numbers

Is there an intractability theorem that says that in any sufficiently rich system for defining really big numbers, there will be two numbers for which it's very, very, ... very difficult to decide ...
James Propp's user avatar
  • 19.7k
2 votes
2 answers
181 views

Background for Kierstead terms

I was looking at some slides of John Longley's here, where he mentions "the Kierstead functional" $$\lambda f.f(\lambda x.f(\lambda y.x)) \ ,$$ (where $f$ should be of type $2$, and $x,y$ of ground ...
Basil's user avatar
  • 269
16 votes
2 answers
3k views

Why is there no product type in simply typed lambda-calculus?

$\DeclareMathOperator\Pair{Pair}\DeclareMathOperator\First{First}\DeclareMathOperator\Second{Second}\DeclareMathOperator\Left{Left}\DeclareMathOperator\Right{Right}\DeclareMathOperator\Choice{Choice}$...
winitzki's user avatar
  • 271
3 votes
1 answer
404 views

Is there an easy decision algorithm for the inhabitation problem for simple types?

Consider the basic system of simple types usually known as $TA_\lambda$. One can prove that (as a consequence of the Subject Reduction Property and the fact that any typable term is strongly $\beta$-...
Alfie's user avatar
  • 31
1 vote
1 answer
169 views

Interaction-based approximation for HP-complete λ-theory?

We are looking for a proof or counter-examples for the following hypothesis. Two combinators $M$ and $N$ are solvable and equivalent in the HP-complete sensible $\lambda$-theory iff either $$ \exists ...
Anton Salikhmetov's user avatar
4 votes
0 answers
635 views

Difference between lambda-calculus with well-formed formulas vs properly-formed formulas

In S.C. Kleene's 1935 paper "$\lambda$-definability and recursiveness," he proves that all $\lambda$-definable functions are general recursive in the Herbrand-Godel sense and vice-versa. However, the ...
mshang's user avatar
  • 141
0 votes
1 answer
429 views

Is it correct to state that basic primitive recursive functions are in fact combinators?

Is it correct saying that the Zero, Successor and Projection functions can be seen as combinators?
NoWhereMan's user avatar