2
$\begingroup$

Programmers do sometimes write a program that creates infinite loop if some particular input is passed into the program.

But Simply-typed lambda calculus has to stop - so the question is, can anyone show some "useful" program in Turing-complete language (e.g. untyped lambda calculus) that does not go into infinite loop but cannot be written in (simply-)typed lambda calculus?

from comment section:

"Yes I know all of these and I know that they are more expressive and those - but halting problem would only have meaning if there is an algorithm (program) that typed ones cannot express - otherwise, we can write all programs into typed one and see whether it is well-formed, right? Then we automatically know whether a program halts or not. This is what I am asking."

Improve this question
$\endgroup$

1 Answer 1

Reset to default
3
$\begingroup$

The distinction isn't just about being able to write non-terminating programs. There are significant differences even between normalizing lambda calculi. For example, consider System F. It's normalizing, so all its programs are terminating (so it's not Turing complete), but it has much more expressive power than the simply-typed lambda calculus (it can express any function that can be proved total in second-order Peano arithmetic).

Perhaps the simplest example is Church numerals. In System F Church numerals can be expressed as terms of type $\forall\alpha. (\alpha\to\alpha)\to(\alpha\to\alpha)$. Each natural number $n$ is then represented as $$\Lambda\alpha.\lambda f:(\alpha\to\alpha).\;\lambda x:\alpha.\; f^n x$$ where $f^n x \equiv \underbrace{f(f(...f}_{n\mbox{-times}} (x)...))$. In the untyped lambda calculus it would be just $\lambda fx.f^n x$.

However, we cannot represent Church numerals and operations on them in the simply typed lambda calculus, because it lacks the necessary polymorphism.

Church numerals can be viewed as one of the simplest recursive data structures. In Haskell we could represent them as 

data Nat = Z | S Nat

foldNat :: Nat -> (r -> r) -> (r -> r)
foldNat Z     f z  = z
foldNat (S n) f z  = f (foldNat n f z)

(Observe that foldNat actually converts our representation into the System-F representation.)

System F and the untyped lambda calculus allow us to represent any (inductive) recursive data structures such as list, trees etc. in the similar way as we represented Church Numerals (see System F Structures). This is not possible in the simply typed lambda calculus - it can express only non-recursive data structures with bounded size.

A good source of information is Proofs and Types by Jean-Yves Girard, Yves Lafont and Paul Taylor.

Improve this answer
$\endgroup$
2
  • $\begingroup$ Yes I know all of these and I know that they are more expressive and those - but halting problem would only have meaning if there is an algorithm (program) that typed ones cannot express - otherwise, we can write all programs into typed one and see whether it is well-formed, right? Then we automatically know whether a program halts or not. This is what I am asking. $\endgroup$
    – user7103
    Mar 2, 2013 at 9:08
  • $\begingroup$ @user7103 This is exactly what typed normalizing calculi are good for. We know that all program expressed in them are terminating. Of course we can't have a calculi that can type exactly all total functions. But we can get "close enough", like in System F we can type exactly those functions that can be proved total in the second-order Peano arithmetic. This covers basically all total functions we can ever imagine. $\endgroup$
    – Petr
    Mar 2, 2013 at 11:18

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.