5
votes
2answers
460 views

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

Consider simply typed $\lambda$-calculus that has only the unit type as primitive. We would like to encode the product and the sum types. An encoding of the product type in the untyped ...
1
vote
0answers
109 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 ...
0
votes
1answer
145 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 ...
0
votes
0answers
100 views

Recursive relation using successor function

What is the recursive relation for H(m)=2^(m^2) using successor function recursive relation for multiplication: mult(x,0)=0; mult(x,S(y))=add(x,mult(x,y)) recursive relation for addition: add(x,0)=x; ...
4
votes
0answers
230 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 ...
0
votes
1answer
242 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?