jrk@sys.uea.ac.uk (Richard Kennaway) (06/08/90)
Time for a change of Subject: line. In message <3539@rex.cs.tulane.edu>, fs@rex.cs.tulane.edu (Frank Silbermann) writes: >You admit you would like to see a different kind of language >-- one in which pattern-matching is accepted at its face value. >You will need a set of constructs which is sufficiently expressive, >and an evaluation procedure which is correct and complete. >Also, you must be able to avoid invalid programs >(e.g. as set of equations which implies 1 = 2). I believe it's been done already. The Huet&Levy paper I mentioned gives the theoretical underpinnings to the equational programming project described in Michael O'Donnell's book "Equational Logic as a Programming Language" (MIT, 1985). [Kennaway] >>>> f Nil Nil = 1 g Nil Nil = 1 >>>> f Nil (Cons x y) = 2 g (Cons x y) Nil = 2 >>>> f (Cons x y) z = 3 g z (Cons x y) = 3 >> if I apply f to Nil, I get a function which maps >> Nil to 1 and (Cons ? ?) to 2. I can also define >> the argument-switching combinator: c x y z = x z y [Silbermann] >First, you must convince me that 'f' and 'g' are functions. >I admit that this program's operational behavior could be >interpreted as the implementation of a few familiar functions, >but do the _formal semantics_ interpret them as such? When I write equations like the above, I think of the equations as defining functions, and that's how they behave. Looks like a duck, quacks like a duck - it's a duck. But I don't have to encode the whole thing in lambda calculus to put that intuition on a formal basis. I can interpret the type declaration list ::= Nil | Cons num list as defining a domain satisfying the isomorphism List = {.} + Num*List (where Num is the flat domain of Miranda numbers.) Then the definitions of f and g can immediately be read as defining functions from List*List to Num. E.g. using the isomorphism above to write List*List = List + Num*List*List = {.} + Num*List + Num*List*List, f maps the three summands to 1, 2, and 3 respectively; so does g, but via a different isomorphism; c takes any function whose domain is List*List and composes it with the swap isomorphism of List*List with itself, and we find that f = c g, as desired. Functions everywhere, and not a lambda in sight. >The term-rewriting I have studied concerns equivalence classes >within a universe of syntactic terms -- functions are never >explicitly mentioned. Here, 'f' and 'g' would be ordinary constructors. That is another, and equally valid, way of thinking of term rewrite systems. It's a question of which view is more useful for the purpose at hand. Hoisting the discussion up a level, people interested in term rewriting seem to divide into two separate cultures. Sometimes, communication between the two is difficult, due to the differing reasons they have for studying rewriting, and resulting from that, the different properties they are interested in, and the different criteria they have for considering some systems "nice" and some "nasty". On one hand are those whose primary interest in equational systems is in using them as functional languages. These people will look at systems of equations like the above and see definitions of domains and functions, and will consider non-left-linear rules, overlapping rules, and systems failing to distinguish operator symbols from constructor symbols as pathological cases of little interest, to be excluded from the class of "nice" rewrite systems. They can be distinguished by their tendency to write "->" instead of "=". :-) On the other hand are people whose interest is in equational specification, who see rules like mult(inv(x),x)=id and f(f(x,y),z)=f(x,f(y,z)) as perfectly reasonable and useful - which, in that context, they are. This is not to say that there is nothing in common between the two, but there is sometimes a tendency for them to talk past each other. -- Richard Kennaway SYS, University of East Anglia, Norwich, U.K. Internet: jrk@sys.uea.ac.uk uucp: ...mcvax!ukc!uea-sys!jrk