On 30/03/15 22:15, Anthony Hall wrote:

Thanks Rob

My problem 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 non-ASCII.


I just don’t think ISO Z got this right.

I’m 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 is avoided.

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 of trouble".

I 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 the world.

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.

I can see the force of that – in fact the “lot of trouble” was precisely having to parse the specification rather than just lex it.


Of course, perhaps one day, the Z Word Tools as a common front-end will also be an option.

The 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!


If 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.


Good luck and best wishes



Proofpower mailing list

Reply via email to