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