On 30/03/15 22:15, Anthony Hall wrote:
is that I need a lexical translation scheme that is not
just specific to Z, but one that makes sense for any of
the open-ended set of languages that ProofPower supports.
I certainly don’t want to translate ASCII characters to
I just don’t
think ISO Z got this right.
certainly not going to disagree with you there!
I don't think ISO is quite right either. Generally in text, I do
think the minus operator (whether prefix or infix) should be the '−'
character (0x2212 MINUS SIGN). I've had the misfortune to write a
lot of technical documents with Word and a normal ASCII dash '-'
(0x2D HYPHEN-MINUS) just isn't wide enough for minus, so I am fairly
used to doing Insert -> Symbol -> Minus sign. In OpenOffice,
ASCII dash is wide enough with a few fixed-width fonts (Courier,
Nimbus Mono L) however with others (Liberation Mono, DejaVu Sans
Mono) it is not and nor is it with variable-width fonts.
With Fuzz, it appers that ASCII '-' (0x2D HYPHEN-MINUS) is mark up
for a full width minus sign, so the problem with writing non-ASCII
It is easy
to design a grammar that allows the same symbol (a minus
sign) to function both as an infix operator and a prefix
operator. However, I failed to realise the importance of
this before the Standards committee ran off and committed
to the backwards incompatible change that gave you “a lot
do sometimes wonder what they thought they were up to. I
think sometimes people get so deep into solving a
problem that they can’t step back and see that the
problem isn’t real at all. As you say, a single symbol
can perfectly well be used – and is, by everyone else in
Spivey uses one symbol for both unary and binary minus but the unary
minus is an ordinary function. Presumably the Standards committee
wanted a template for unary minus so that, for example,
− − x
is not parsed as
(− −) x
which seems sensible. The Standard also requires that the mapping
from operator words in templates to tokens is a function. This
prevents '−' from being both the PRE and I tokens, so can't be used
in both prefix and infix templates. The reason for this, I suspect,
is all tied up with the Z concrete syntax: using '−' for both prefix
and infix minus would make
f − x
ambiguous — is that
App (f, − x)
App (_ − _, (f, x))
Tightening up the concrete syntax to allow operator words to be
reused in templates would require a little thought. Alternatively,
perhaps operator words could be reused by defining a fixed
precedence on operator word tokens with the same word, for example,
an I token takes priority over a PRE token. After all,
f − x
should never be parsed as
f (− x)
As I said in
a recent post to Phil Clayton, I abandoned my half-hearted
hopes of providing Unicode support for ProofPower in
general and some level of interoperability between
ProofPower-Z and ISO Z at the same time. Inside
ProofPower, interoperability with ISO Z and ProofPower-Z
is best implemented using parsed syntax trees rather than
lexical token streams.
can see the force of that – in fact the “lot of trouble”
was precisely having to parse the specification rather
than just lex it.
perhaps one day, the Z Word Tools as a common front-end
will also be an option.
trouble is that to go from ProofPower to ISO Z that
translation would have to be done, and again I would
have to have a parse tree from ProofPower to do it. I
haven’t thought any more since our conversations of
years ago about how a ZWT / Proofpower interface might
work (and maybe such a thing wouldn’t be useful anyway),
so my post was a bit of a knee-jerk reaction hoping to
forestall a difficulty that will surely arise if we were
ever to attempt such a thing. But I understand that
force of your argument. The problem is certainly on the
ISO Z side, and not of ProofPower’s makng!
you do ever think a Word interface would be useful, do
get in touch, but I won’t hold my breath. I’ve not done
any development on ZWT for ages – I don’t know whether
anyone is using it in anger, though it still has a
trickle of downloads.
luck and best wishes