I think the Majority function is a good example to convince you.
(We can have many similar examples).
maj :: Bool -> Bool -> Bool -> Bool
maj True True True = True
maj True False b = b
maj False b True = b
maj b True False = b
maj False False False = False
For this function, there is NOT a way to define it as the form
maj x y z = Elim_Bool .......
and satisfy all the five equations (computationally).
That is true, but why would we care? As Conor pointed out maj was only
constructed with the goal to show that not all functions are definable
by case-splittings and moreover it is easy to define a function which
is extensionally equivalent to maj.
When would you need the equations above to hold definitionally?
What are your other examples?
But if we allow partially defined functions and pattern matching, the
Majority function can be defined as it is.
To me pattern matching is a shorthand for case-splitting.
Cheers,
Thorsten
--
Dr. Thorsten Altenkirch phone : (+44) (0)115 84 66516
Lecturer http://www.cs.nott.ac.uk/~txa/
School of Computer Science & IT University of Nottingham
This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.
