Anthony, On 30 Mar 2015, at 17:54, Anthony Hall <[email protected]> wrote:
> Dear Rob > > I have just one small query - about the minus sign problem Thanks for your interest. > > I had a lot of trouble with this, as you might expect, when translating > between Spivey latex and standard Z, but it can be done. 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 don’t know whether translating from Proofpower is more difficult, but it > would be nice to get this right if possible while you are translating to > Unicode. I just don’t think ISO Z got this right. 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". > Or am I missing something? 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. Of course, perhaps one day, the Z Word Tools as a common front-end will also be an option. > > All the best And to you! Rob. > > Anthony > > > From: Proofpower [mailto:[email protected]] On Behalf Of Rob > Arthan > Sent: 28 March 2015 16:03 > To: ProofPower List > Subject: [ProofPower] Updated Unicode translation scheme > > Dear All, > > Acting on some very helpful comments from Phil Clayton, I have revised the > proposed scheme for translating between Unicode and the ProofPower extended > character set. The revised scheme is described here: > > http://www.lemma-one.com/ProofPower/unicode/pp-unicode.html > > (You can find the earlier version at > http://www.lemma-one.com/ProofPower/unicode/v0/pp-unicode.html) > > The new scheme for you to look at with your e-mail client follows below. > > As before, Mac OS X supports all the necessary glyphs. If you install the > STIX fonts on Linux (stix-fonts on Fedora, fonts-stix on Ubuntu), there is > now a good chance that you will have all you need. > > Any feedback will be much appreciated. > > Regards, > > Rob. > > > 0x80: %subset%: ⊆ > 0x81: %rsub%: ⩥ > 0x82: %bagunion%: ⨄ > 0x83: %bbU%: 𝕌 > 0x84: %Delta%: 𝛥 > 0x85: %fcomp%: ∘ > 0x86: %Phi%: 𝛷 > 0x87: %Gamma%: 𝛤 > 0x88: %EZ%: └ > 0x89: %down%: ⋎ > 0x8A: %Theta%: 𝛩 > 0x8B: %dcat%: ⁀/ > 0x8C: %Lambda%: 𝛬 > 0x8D: %mem%: ∈ > 0x8E: %notmem%: ∉ > 0x8F: %bij%: ⤖ > 0x90: %Pi%: 𝛱 > 0x91: %SML%: ⓜ > 0x92: %rres%: ▷ > 0x93: %Sigma%: 𝛴 > 0x94: %<:%: ⓣ > 0x95: %Upsilon%: 𝛶 > 0x96: %boolean%: 𝔹 > 0x97: %Omega%: 𝛺 > 0x98: %Xi%: 𝛯 > 0x99: %Psi%: 𝛹 > 0x9A: %emptyset%: ∅ > 0x9B: %up%: ⋏ > 0x9C: %BHH%: ═ > 0x9D: %SZG%: ╒ > 0x9E: %finj%: ⤕ > 0x9F: %ffun%: ⇻ > 0xA0: %psubset%: ⊂ > 0xA1: %intersect%: ∩ > 0xA2: %rseq%: ⟩ > 0xA3: %symdiff%: ⊖ > 0xA4: %equiv%: ⇔ > 0xA5: %dintersect%: ⋂ > 0xA6: %def%: ≜ > 0xA7: %lseq%: ⟨ > 0xA8: %lrelimg%: ⦇ > 0xA9: %rrelimg%: ⦈ > 0xAA: %rel%: ↔ > 0xAB: %overwrite%: ⊕ > 0xAC: %<%: ⌜ > 0xAD: %fun%: → > 0xAE: %>%: ⌝ > 0xAF: %real%: ℝ > 0xB0: %EFT%: ■ > 0xB1: %and%: ∧ > 0xB2: %or%: ∨ > 0xB3: %not%: ¬ > 0xB4: %implies%: ⇒ > 0xB5: %forall%: ∀ > 0xB6: %exists%: ∃ > 0xB7: %spot%: ⦁ > 0xB8: %x%: × > 0xB9: %SFT%: Ⓢ > 0xBA: %bigcolon%: ⦂ > 0xBB: %rcomp%: ⨾ > 0xBC: %leq%: ≤ > 0xBD: %neq%: ≠ > 0xBE: %geq%: ≥ > 0xBF: %symbol%: 𝕊 > 0xC0: %union%: ∪ > 0xC1: %alpha%: 𝛼 > 0xC2: %beta%: 𝛽 > 0xC3: %refinedby%: ⊑ > 0xC4: %delta%: 𝛿 > 0xC5: %select%: 𝜀 > 0xC6: %phi%: 𝜑 > 0xC7: %gamma%: 𝛾 > 0xC8: %eta%: 𝜂 > 0xC9: %iota%: 𝜄 > 0xCA: %theta%: 𝜃 > 0xCB: %kappa%: 𝜅 > 0xCC: %fn%: 𝜆 > 0xCD: %mu%: 𝜇 > 0xCE: %nu%: 𝜈 > 0xCF: %psurj%: ⤀ > 0xD0: %pi%: 𝜋 > 0xD1: %chi%: 𝜒 > 0xD2: %rho%: 𝜌 > 0xD3: %sigma%: 𝜎 > 0xD4: %tau%: 𝜏 > 0xD5: %upsilon%: 𝜐 > 0xD6: %complex%: ℂ > 0xD7: %omega%: 𝜔 > 0xD8: %xi%: 𝜉 > 0xD9: %psi%: 𝜓 > 0xDA: %zeta%: 𝜁 > 0xDB: %SX%: ⦏ > 0xDC: %BV%: │ > 0xDD: %EX%: ⦎ > 0xDE: %dunion%: ⋃ > 0xDF: %pfun%: ⇸ > 0xE0: %inj%: ↣ > 0xE1: %dsub%: ⩤ > 0xE2: %bottom%: ⊥ > 0xE3: %Leftarrow%: ⇐ > 0xE4: %psupset%: ⊃ > 0xE5: %supset%: ⊇ > 0xE6: %fset%: 𝔽 > 0xE7: %uptext%: ↗ > 0xE8: %dntext%: ↘ > 0xE9: %replacedby%: ≡ > 0xEA: %cantext%: ↕ > 0xEB: %cat%: ⁀ > 0xEC: %extract%: ↿ > 0xED: %map%: ↦ > 0xEE: %nat%: ℕ > 0xEF: %surj%: ↠ > 0xF0: %pset%: ℙ > 0xF1: %SZT%: ⓩ > 0xF2: %dres%: ◁ > 0xF3: %rat%: ℚ > 0xF4: %thm%: ⊢ > 0xF5: %ulbegin%: ⨽ > 0xF6: %ulend%: ⨼ > 0xF7: %BT%: ├ > 0xF8: %uminus%: ﹣ > 0xF9: %filter%: ↾ > 0xFA: %int%: ℤ > 0xFB: %lbag%: ⟦ > 0xFC: %BH%: ─ > 0xFD: %rbag%: ⟧ > 0xFE: %pinj%: ⤔ > 0xFF: %SZS%: ┌ > > _______________________________________________ > Proofpower mailing list > [email protected] > http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
_______________________________________________ Proofpower mailing list [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
