Anthony,

On 30 Mar 2015, at 17:54, Anthony Hall <anth...@anthonyhall.org> 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:proofpower-boun...@lemma-one.com] 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
> Proofpower@lemma-one.com
> http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to