🚀 go-pugleaf

In article <1535@sys.uea.ac.uk> jrk@sys.uea.ac.uk (Richard Kennaway) writes:
>
>	Functional languages are supposed to be readable as mathematics.
>	For languages such as Miranda, ML, Haskell, etc. this means
>	that one should be able to read a program such as that below
>	as a set of equational axioms.
>
>    list  ::=  Nil  |  Cons num list
>
>    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
>
>    loop              = loop

You are suggesting that the Miranda's semantics should reflect
the equational notation.  Actually, the logic is not equational;
Miranda permits contradictory program clauses, which are resolved
by the evaluation order.

The clausal notation, which incorporates pattern-matching,
is only a syntactic sugar.  I find pattern-matching
a convenient shortcut when hacking, but when thinking about
denotational semantics, I first compile such syntactic sugars
out of my examples.

>	Notice that f and g are nearly the same function,
>	but they take their arguments in the opposite order.
>	(The results differ in some cases, therefore Miranda's
>	evaluation strategy is not quite correct.)

Only if you take the syntactic sugars literally.

>	... the basic algorithm for dealing _properly_
>	with systems like the above ...(can be found in)...  Huet & Levy
>	"Call by need computations in non-ambiguous linear
>	term rewriting systems", INRIA report 359, 1979.

You are advocating a different kind of language.
If you want to interpret a Miranda program as a
non-ambiguous linear term rewriting system,
you will need a way to prevent contradictions in the equations
(which Miranda permits).  Also, I doubt that the paper you cite
takes higher-order functions into consideration.

	Frank Silbermann	fs@rex.cs.tulane.edu
	Tulane University, New Orleans, Louisianna, U.S.A.