Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!usc!samsung!uunet!munnari.oz.au!bunyip.cc.uq.oz.au!uqcspe!cs.uq.oz.au!brendan
From: brendan@cs.uq.oz.au (Brendan Mahony)
Newsgroups: comp.specification.z
Subject: Re: Prove me wrong
Message-ID: <2235@uqcspe.cs.uq.oz.au>
Date: 1 Jul 91 00:24:13 GMT
References: <1991Jun28.175058.4987@agate.berkeley.edu> <2232@uqcspe.cs.uq.oz.au>
Sender: news@cs.uq.oz.au
Reply-To: brendan@cs.uq.oz.au
Lines: 59


In <1991Jun28.175058.4987@agate.berkeley.edu> bks@lima.berkeley.edu (Bradley K. Sherman) writes:


>>Back to the drawing board and come up with an unambiguous syntax
>>expressible in the intersection of the ASCII and EBCDIC codes
>>and we can make some progress.

In <2232@uqcspe.cs.uq.oz.au> david@cs.uq.oz.au (David Duke) writes:
>Whats ambiguous about the syntax?  There are several type checkers available
>for Z (for example, `Fuzz' by Mike Spivey at the PRG, Oxford Uni); there is
>also a syntax-based editor at UQ -- all of which need a precise syntax on
>which to work!

I am afraid this is not much of an argument. Both these parsers use a
restricted Z grammar. Yes I know Spivey's is "definitive", but it is still
a re-engineering of the language and is much more restrictive than what
people used to write down before there was an official syntax. The UQ
grammar (and it seems the Spivey one) is a linearised version of Z. This
means that you either have to put in more brackets than you would like,
or you must define precedents between operators that cannot interfer
semantically, such as + and union or more importantly function
application and function application.

An expression like

	f g a

can generally only mean one thing, either

	f : (X -> Y) -> (A -> B)
	g : X -> Y
	a : A
	f g a = (f(g))(a) : B
					example: f^3 x
or

	f : Y -> Z
	g : X -> Y
	a : X
	f g a = f(g(a)) : Z
					example: sin cos x

If either meaning is clear from the context, then the parser should
chose the right one regardless of precedent information. You should not
have to put brackets in to "force" the parser to read it the right way.

If neither meaning is clear from the context, for example an expression
involving type conformant expressions such as

	{} {} {}

then your really do have an ambiguity and it should be flagged as such
and not hidden by magical precedent applications.
--
Brendan Mahony                   | brendan@batserver.cs.uq.oz       
Department of Computer Science   | heretic: someone who disgrees with you
University of Queensland         | about something neither of you knows
Australia                        | anything about.