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!


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.

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 


Good luck and best wishes





Proofpower mailing list

Reply via email to