Typed lambda calculus, recursion and halting 
Author Message
 Typed lambda calculus, recursion and halting

I am implementing a type system for a Turner style combinator graph
reduction system, based on Turner's paper
"A New Implementation Technique For Applicative Languages"
and was working through Roger Hindley's book "Basic Simple Type Theory".

He proves the Weak Normalization Theorem, that every typable lambda calculus
term has a beta-normal form. This means that we can alway find a beta
reduction sequence that halts at a normal form.

I was wondering how this result relates to the halting problem. Since Turing
provided one of the first proofs of the Weak Normalization Theorem, typable
terms cannot relate directly to halting computations. Does this mean that
the typable terms somehow miss the interesing part of the lambda calculus
where untypable terms may or may not have a normal form?

In particular, the fixed-point combinator Y is not typable, because it has
no normal form.

However, looking at Robin Milner's 1978 paper "A Theory of Type Polymorphism
in Programming", while he acknowledges that Y cannot be given a type, he is
able to introduce "fix" syntax which allows for recursive definitions and
assign types to such expressions. While maintaining the property that typed
programs cannot go wrong from a type point of view, presumably they can now
"go wrong" by not terminating.

It seems that typing of recursive programs using fix is possible because we
are always dealing with a particular instance, and not a general fixed-point
operator like Y. (In the same way as general self application, as in (lambda
x . x x) is not typable, but some particular cases, such as (I I) or (K K)
are?)

So, to finally get to my question -

Is it possible to define a set of pure combinators (e.g. SKIY and no
variables) and an abstraction process to remove variables from a language
such as the one Milner uses, in such a way that type checking can be
performed on the "compiled" combinator translation with the same result as
if it was performed on the original program? The problem being: how to
translate recursive definitions.



Wed, 14 May 2003 07:04:22 GMT  
 Typed lambda calculus, recursion and halting

Quote:
> Is it possible to define a set of pure combinators (e.g. SKIY and no
> variables) and an abstraction process to remove variables from a language
> such as the one Milner uses, in such a way that type checking can be
> performed on the "compiled" combinator translation with the same result as
> if it was performed on the original program? The problem being: how to
> translate recursive definitions.

I'm pretty sure it's possible -- all you need to do is introduce
recursive types and get back to the D ~ D->D domain underlying
the untyped lambda calculus.

-Greg



Thu, 15 May 2003 03:00:00 GMT  
 
 [ 2 post ] 

 Relevant Pages 

1. Recursion in the Lambda Calculus

2. Typed Lambda calculus

3. history of (typed) lambda calculus

4. Type-free Lambda Calculus: paradoxes

5. Tagged variables in typed lambda-calculus - references?

6. Why was typed lambda calculus not used?

7. Lambda Calculus Question

8. lambda calculus implementation

9. Introduction to lambda calculus ?

10. Lambda Calculus Problem!

11. Negativism and division in lambda-calculus

12. Lambda calculus + Church numerals

 

 
Powered by phpBB® Forum Software