[<<][compsci][>>][..]

Sun Mar 7 21:19:03 CET 2010

## Simply Typed LC is Strongly Normalizing

From [1]:
Given the standard semantics, the simply typed lambda calculus is
strongly normalizing: that is, well-typed terms always reduce to a
value, i.e., a lambda abstraction. This is because recursion is not
allowed by the typing rules. Recursion can be added to the language
by either having a special operator of type (a->a)->a or adding
general recursive types, though both eliminate strong normalization.
Since it is strongly normalizing, it is decidable whether or not a
simply typed lambda calculus program halts: it does! We can
therefore conclude that the language is not Turing complete.
In Haskell and OCaml the type inferencer doesn't like construction
of infinite types:
:t (\x -> x x) (\x -> x x)
To express the Y combinator in this direct form requires it to be
wrapped in a recursive type[3] (quotes from [2]):
The problem with fix f = (\x -> f (x x))(\x -> f (x x)) is that one
needs a solution to the type equation b = b -> a. Fortunately this
can be done with Haskellâ€™s data types.
> newtype Mu a = Roll { unroll :: Mu a -> a }
> fix f = (\x -> f ((unroll x) x)) (Roll (\x -> f ((unroll x) x)))
Of course, this is just an academic exercise. To actually define a
fixpoint combinator in Haskell, one would use recursive definitions.
I.e. the Y combinator can be defined directly in its recursive form:
> y f = f (y f)
[1] http://en.wikipedia.org/wiki/Simply_typed_lambda_calculus
[2] http://r6.ca/blog/20060919T084800Z.html
[3] http://en.wikipedia.org/wiki/Recursive_type
[4] http://en.wikipedia.org/wiki/System_F

[Reply][About]

[<<][compsci][>>][..]