Why use Turing Machines when there's Haskell

Predicates and algorithms in Haskell

The nice thing about using Haskell (or lambda calculus) against using Turing machines is the possibility to talk about signatures of predicates and/or algorithms in a more natural manner. It is even easier to describe languages in terms of partial predicates rather than grammars or TMs.

So, let's do that:

A one-place predicate (1pp) P is defined by a Haskell expression of the form

P :: String -> Bool
P = \x -> ...

returning either True or False. Since Haskell allows for Type Synonyms, we define as an abbreviation:

type OnePP = String -> Bool

The extension or language of the predicate P - denoted as L(P) - is given by those values for which P returns True. If P returns True or False for every argument, it is called total and can be regarded as a decision procedure for L(P), else it called partial and can be regarded as an acceptor, recognizer, semi-decider or enumeration procedure for L(P).

If a language L = L(P) for a 1pp P, we refer to P as a representation of L.

Note that when we will talk about decision problems regarding languages, we assume the language in question is given by a representation. Another representation could be a Turing Machine, Type-0 grammar or another equivalent formalism.


Examples

The Acceptance Problem A_TM can now be stated and proved like this:

Problem: Is there a total predicate

H :: OnePP -> String -> Bool

such that (H A w) returns True, iff A returns True for w and False, if not (i. e. A returns False or no value at all)

Answer: No.

Proof: Assume H exists as specified. Then consider the following Haskell program:

D :: OnePP -> Bool
D = \A -> not (H A A)

Then the program

main = (D D)

shows the desired contradiction.

The fact that A_TM is recursively enumerated is neatly shown by

Acc :: OnePP -> String -> Bool
Acc = \A w -> (A w)

That should work nicely - more about that when Rice's Theorem comes up in some days...