Unicode Mapping for ProofPower

The mapping is defined in terms of a basic translation table, which, subject to some additional rules, defines a translation from ProofPower to Unicode or from Unicode to ProofPower. There are some notes giving the rationale for the mapping.

Basic Translation Table

The following table gives a one-to-one mapping from a subset of the ProofPower extended character set to the Unicode character set. The range of the mapping includes all the ProofPower extended characters with the exception of the byte 0x8B.

The LaTeX column contains GIFs showing the typeset form of each character (produced using dvipng). The GIFs should display properly in any browser without any Unicode support. The Unicode column shows the corresponding Unicode glyph as rendered by your web browser.

Byte LaTeX Unicode Code Point Unicode Name

0x80 ⊆ 0x002286 SUBSET OF OR EQUAL TO

0x81 ⩥ 0x002A65 Z NOTATION RANGE ANTIRESTRICTION

0x82 ⨄ 0x002A04 N-ARY UNION OPERATOR WITH PLUS

0x83 𝕌 0x01D54C MATHEMATICAL DOUBLE-STRUCK CAPITAL U

0x84 Δ 0x000394 GREEK CAPITAL LETTER DELTA

0x85 ∘ 0x002218 RING OPERATOR

0x86 Φ 0x0003A6 GREEK CAPITAL LETTER PHI

0x87 Γ 0x000393 GREEK CAPITAL LETTER GAMMA

0x88 └ 0x002514 BOX DRAWINGS LIGHT UP AND RIGHT

0x89 ⋎ 0x0022CE CURLY LOGICAL OR

0x8A Θ 0x000398 GREEK CAPITAL LETTER THETA

0x8B Translated into a sequence of two code points. See below

0x8C Λ 0x00039B GREEK CAPITAL LETTER LAMDA

0x8D ∈ 0x002208 ELEMENT OF

0x8E ∉ 0x002209 NOT AN ELEMENT OF

0x8F ⤖ 0x002916 RIGHTWARDS TWO-HEADED ARROW WITH TAIL

0x90 Π 0x0003A0 GREEK CAPITAL LETTER PI

0x91 🄼 0x01F13C SQUARED LATIN CAPITAL LETTER M

0x92 ▷ 0x0025B7 WHITE RIGHT-POINTING TRIANGLE

0x93 Σ 0x0003A3 GREEK CAPITAL LETTER SIGMA

0x94 🅃 0x01F143 SQUARED LATIN CAPITAL LETTER T

0x95 Υ 0x0003A5 GREEK CAPITAL LETTER UPSILON

0x96 𝔹 0x01D539 MATHEMATICAL DOUBLE-STRUCK CAPITAL B

0x97 Ω 0x0003A9 GREEK CAPITAL LETTER OMEGA

0x98 Ξ 0x00039E GREEK CAPITAL LETTER XI

0x99 Ψ 0x0003A8 GREEK CAPITAL LETTER PSI

0x9A ∅ 0x002205 EMPTY SET

0x9B ⋏ 0x0022CF CURLY LOGICAL AND

0x9C ═ 0x002550 BOX DRAWINGS DOUBLE HORIZONTAL

0x9D ╒ 0x002552 BOX DRAWINGS DOWN SINGLE AND RIGHT DOUBLE

0x9E ⤕ 0x002915 RIGHTWARDS ARROW WITH TAIL WITH DOUBLE VERTICAL STROKE

0x9F ⇻ 0x0021FB RIGHTWARDS ARROW WITH DOUBLE VERTICAL STROKE

0xA0 ⊂ 0x002282 SUBSET OF

0xA1 ∩ 0x002229 INTERSECTION

0xA2 〉 0x003009 RIGHT ANGLE BRACKET

0xA3 ⊖ 0x002296 CIRCLED MINUS

0xA4 ⇔ 0x0021D4 LEFT RIGHT DOUBLE ARROW

0xA5 ⋂ 0x0022C2 N-ARY INTERSECTION

0xA6 ≜ 0x00225C DELTA EQUAL TO

0xA7 〈 0x003008 LEFT ANGLE BRACKET

0xA8 ⦇ 0x002987 Z NOTATION LEFT IMAGE BRACKET

0xA9 ⦈ 0x002988 Z NOTATION RIGHT IMAGE BRACKET

0xAA ↔ 0x002194 LEFT RIGHT ARROW

0xAB ⊕ 0x002295 CIRCLED PLUS

0xAC ⌜ 0x00231C TOP LEFT CORNER

0xAD → 0x002192 RIGHTWARDS ARROW

0xAE ⌝ 0x00231D TOP RIGHT CORNER

0xAF ℝ 0x00211D DOUBLE-STRUCK CAPITAL R

0xB0 █ 0x002588 FULL BLOCK

0xB1 ∧ 0x002227 LOGICAL AND

0xB2 ∨ 0x002228 LOGICAL OR

0xB3 ¬ 0x0000AC NOT SIGN

0xB4 ⇒ 0x0021D2 RIGHTWARDS DOUBLE ARROW

0xB5 ∀ 0x002200 FOR ALL

0xB6 ∃ 0x002203 THERE EXISTS

0xB7 ⦁ 0x002981 Z NOTATION SPOT

0xB8 × 0x0000D7 MULTIPLICATION SIGN

0xB9 Ⓢ 0x0024C8 CIRCLED LATIN CAPITAL LETTER S

0xBA ⦂ 0x002982 Z NOTATION TYPE COLON

0xBB ⨾ 0x002A3E Z NOTATION RELATIONAL COMPOSITION

0xBC ≤ 0x002264 LESS-THAN OR EQUAL TO

0xBD ≠ 0x002260 NOT EQUAL TO

0xBE ≥ 0x002265 GREATER-THAN OR EQUAL TO

0xBF 𝕊 0x01D54A MATHEMATICAL DOUBLE-STRUCK CAPITAL S

0xC0 ∪ 0x00222A UNION

0xC1 α 0x0003B1 GREEK SMALL LETTER ALPHA

0xC2 β 0x0003B2 GREEK SMALL LETTER BETA

0xC3 ⊑ 0x002291 SQUARE IMAGE OF OR EQUAL TO

0xC4 δ 0x0003B4 GREEK SMALL LETTER DELTA

0xC5 ϵ 0x0003F5 GREEK LUNATE EPSILON SYMBOL

0xC6 ϕ 0x0003D5 GREEK PHI SYMBOL

0xC7 γ 0x0003B3 GREEK SMALL LETTER GAMMA

0xC8 η 0x0003B7 GREEK SMALL LETTER ETA

0xC9 ι 0x0003B9 GREEK SMALL LETTER IOTA

0xCA θ 0x0003B8 GREEK SMALL LETTER THETA

0xCB κ 0x0003BA GREEK SMALL LETTER KAPPA

0xCC λ 0x0003BB GREEK SMALL LETTER LAMDA

0xCD μ 0x0003BC GREEK SMALL LETTER MU

0xCE ν 0x0003BD GREEK SMALL LETTER NU

0xCF ⤀ 0x002900 RIGHTWARDS TWO-HEADED ARROW WITH VERTICAL STROKE

0xD0 π 0x0003C0 GREEK SMALL LETTER PI

0xD1 χ 0x0003C7 GREEK SMALL LETTER CHI

0xD2 ρ 0x0003C1 GREEK SMALL LETTER RHO

0xD3 σ 0x0003C3 GREEK SMALL LETTER SIGMA

0xD4 τ 0x0003C4 GREEK SMALL LETTER TAU

0xD5 υ 0x0003C5 GREEK SMALL LETTER UPSILON

0xD6 ℂ 0x002102 DOUBLE-STRUCK CAPITAL C

0xD7 ω 0x0003C9 GREEK SMALL LETTER OMEGA

0xD8 ξ 0x0003BE GREEK SMALL LETTER XI

0xD9 φ 0x0003C6 GREEK SMALL LETTER PHI

0xDA ζ 0x0003B6 GREEK SMALL LETTER ZETA

0xDB ⦏ 0x00298F LEFT SQUARE BRACKET WITH TICK IN BOTTOM CORNER

0xDC │ 0x002502 BOX DRAWINGS LIGHT VERTICAL

0xDD ⦎ 0x00298E RIGHT SQUARE BRACKET WITH TICK IN BOTTOM CORNER

0xDE ⋃ 0x0022C3 N-ARY UNION

0xDF ⇸ 0x0021F8 RIGHTWARDS ARROW WITH VERTICAL STROKE

0xE0 ↣ 0x0021A3 RIGHTWARDS ARROW WITH TAIL

0xE1 ⩤ 0x002A64 Z NOTATION DOMAIN ANTIRESTRICTION

0xE2 ⊥ 0x0022A5 UP TACK

0xE3 ⇐ 0x0021D0 LEFTWARDS DOUBLE ARROW

0xE4 ⊃ 0x002283 SUPERSET OF

0xE5 ⊇ 0x002287 SUPERSET OF OR EQUAL TO

0xE6 𝔽 0x01D53D MATHEMATICAL DOUBLE-STRUCK CAPITAL F

0xE7 ↗ 0x002197 NORTH EAST ARROW

0xE8 ↘ 0x002198 SOUTH EAST ARROW

0xE9 ≡ 0x002261 IDENTICAL TO

0xEA ↕ 0x002195 UP DOWN ARROW

0xEB ⁀ 0x002040 CHARACTER TIE

0xEC ↿ 0x0021BF UPWARDS HARPOON WITH BARB LEFTWARDS

0xED ↦ 0x0021A6 RIGHTWARDS ARROW FROM BAR

0xEE ℕ 0x002115 DOUBLE-STRUCK CAPITAL N

0xEF ↠ 0x0021A0 RIGHTWARDS TWO HEADED ARROW

0xF0 ℙ 0x002119 DOUBLE-STRUCK CAPITAL P

0xF1 🅉 0x01F149 SQUARED LATIN CAPITAL LETTER Z

0xF2 ◁ 0x0025C1 WHITE LEFT-POINTING TRIANGLE

0xF3 ℚ 0x00211A DOUBLE-STRUCK CAPITAL Q

0xF4 ⊢ 0x0022A2 RIGHT TACK

0xF5 ₍ 0x00208D SUBSCRIPT LEFT PARENTHESIS

0xF6 ₎ 0x00208E SUBSCRIPT RIGHT PARENTHESIS

0xF7 ├ 0x00251C BOX DRAWINGS LIGHT VERTICAL AND RIGHT

0xF8 ﹣ 0x00FE63 SMALL HYPHEN-MINUS

0xF9 ↾ 0x0021BE UPWARDS HARPOON WITH BARB RIGHTWARDS

0xFA ℤ 0x002124 DOUBLE-STRUCK CAPITAL Z

0xFB ⟦ 0x0027E6 MATHEMATICAL LEFT WHITE SQUARE BRACKET

0xFC ─ 0x002500 BOX DRAWINGS LIGHT HORIZONTAL

0xFD ⟧ 0x0027E7 MATHEMATICAL RIGHT WHITE SQUARE BRACKET

0xFE ⤔ 0x002914 RIGHTWARDS ARROW WITH TAIL WITH VERTICAL STROKE

0xFF ┌ 0x00250C BOX DRAWINGS LIGHT DOWN AND RIGHT

ProofPower to Unicode

Translating ProofPower into Unicode converts a stream of bytes into a stream of Unicode code points. An ASCII string of the form "%xHHHHHH%", where HHHHHH is a string of 6 upper-case hexadecimal digits representing a value in the range 0x000100 to 0x10FFFF, is translated into the Unicode code point with that value. Strings of this form are identified reading from left to right. Any byte in the range 0x00 to 0x7F not appearing in such a string is translated into the Unicode code point with the same numeric value. A byte in the range 0x80 to 0xFF other than 0x8B is translated into the Unicode code point identified in the basic translation table above. The byte 0x8B (representing distributed concatenation in Z) is translated into the sequence of 2 Unicode code points shown below:

Byte	LaTeX	Code Point Sequence	Unicode
0x8B		0x002040 0x00002F	⁀/

Unicode to ProofPower

Translating Unicode converts a stream of code points into a stream of bytes. A Unicode code point in the range 0x000000 to 0x00007F is translated into the byte with the same numeric value. A Unicode code point listed in the Code Point column in the basic translation table is translated into the byte with the numeric value given in the Byte column. A Unicode code point in the range 0x000080 to 0x10FFFF that is not listed in the basic translation table is translated into the ASCII string "%xHHHHHH%", where HHHHHH represents the value of the code point as 6 upper-case hexadecimal digits.

Rationale

The mapping for Z symbols (other than paragraph mark-up) follows the ISO Z Standard Unicode mark-up. An exception is that the ASCII minus sign is translated unchanged while the unary minus sign 0xF8 is translated into SMALL HYPHEN-MINUS. Unfortunately, SMALL HYPHEN-MINUS often seems to be rendered bigger than HYPHEN-MINUS.

Unicode does not provide any single glyphs that resemble the decorated Quine corners provided in the ProofPower character set for quoting HOL types, ML and Z. Squared letters T, M and Z have been used as a convenient single character translation for these.

The %xHHHHHH% format allows any code point to be used in a ProofPower identifier. Strings of this form are highly unlikely to occur in existing scripts and so there is no requirement for a string of this form to be translated into Unicode as 9 ASCII characters.

Created by Rob Arthan [rda at lemma-one dot com]

Last updated: 11th March 2015