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 ...
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 ...
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 ...
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; ...
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 ...
Is it correct saying that the Zero, Successor and Projection functions can be seen as combinators?