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."

$\endgroup$
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.

$\endgroup$
  • $\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 '13 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 Pudlák Mar 2 '13 at 11:18

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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