Typed Turing-complete combinators?
Author Message
Typed Turing-complete combinators?

It's well-known that the set of combinators S, K, and I
are Turing-complete.  (And, of course, you don't need I,
as I = S K K.) However, in my mind they correspond
to the untyped lambda calculus, as the type needed for S
in this doesn't fit into the usual restrictions of the Hindley-Milner
type systems found in SML and Haskell.

That is, if we define, in Haskell (where we can't use the usual capitals):

Quote:
> i x = x
> k c x = c
> s f g x = ((f x) (g x))

Then Haskell gives the s combinator given the following type:
s :: (a -> b -> c) -> (a -> b) -> a -> c
Unfortunately, this isn't general enough, as it assumes that
x is a monomorphic function.  Thus the terms like
((s i) i)
don't typecheck.

That's all well-known and a standard limitation of the Hindley-Milner
type system.

Suppose we want to live within that type system,
and suppose we give ourselves a recursion operator as a primitive,
as we must to get Turing-completeness.  Call this recursion primitive "fix",
and define its semantics by:

Quote:
> fix g = g (fix g)

Now, my question is this.  What's a minimal set of other combinators
needed to get Turing-completeness, assuming we have "fix" and want
to use combinators with their types given by Hindley-Milner?
I'm looking for "interesting" sets of combinators to show my students.
S and K are interesting, but do they work in such a typed context also?
I'm sure that there must be others that are equally neat.

Gary T. Leavens

--
Department of Computer Science, Iowa State University
229 Atanasoff Hall, Ames, Iowa 50011-1040 USA

URL: http://www.*-*-*.com/ ~leavens

Tue, 31 Jul 2001 03:00:00 GMT

 Page 1 of 1 [ 1 post ]

Relevant Pages