(Last modified: 20040910)
This program implements Navara's graphical method for evaluating expressions in orthomodular lattices (OMLs in short) ([1]). This method allows to check in simple way whether some identities hold in OMLs. Not every identity can be checked by this method. The following restrictions are applied:
If the identity contains up to two variables, it can be evaluated by this method without any restriction. (In this case we use the computation in the free orthomodular lattice generated by two generators denoted F(a,b). These generators are denoted by a and b in the program. This lattice has 96 elements and its structure can be depicted by images. For more details, see [1] for the method for creating such images and [1], [2] for the structure of this lattice.)
For identities with more than two variables, there should be only one pair of incompatible elements and all other elements commute with every element in the lattice. Such commutative elements are denoted as ci in the program. ( This restriction is because the free OML with more than 2 generators need not be finite. These commutative elements cause that the structure of the OML can be expressed as a direct product of 2n copies of F(a,b), where n is the number of compatible elements ci. For more information see [1].)
Types of expressions which can be evaluated by the program:
The return value is the atomic representation of the element expressed in Navara's graphical representation, plain TeX macro and its Beran's number.
The return value of these operations is True or False.
rel1 IMEQ rel2,
The return value of these relations is True or False.
The example of output for the expression a v b: (line numbers added for referring)
No.of.gen: 0 <- Number of elements ci RPN: abv <- Reverse Polish Notation of the expression ------- \ | o | \ | x x | - Navara's graphic representation (see [1]) | x | / ------- / \nc0111|| <- TeX macro for typesetting the graphical representation (foml2.sty) Beran's number of the element: 92 <- Beran's number of the expression (see [2])If the number of the elements ci is not equal to 0, then the output contains comma separated list of graphic representations, TeX macros and Beran's numbers of the expression, as shown below.
No.of.gen: 2 RPN: c1b^c2a^v ------- o | o o | | o | o o , | x o , o x | , | x x | o | x x | | x | ------- ------- ------- \nc0000--, \nc0101|_, \nc0011_|, \nc0111|| Beran's numbers of components: 1, 22, 39, 92
if (a = a), then (a = a ^ (a ^ b)') or (a = a ^ (a ^ b')') (True implies False, i.e. False)
a = a => a = (a ^(a ^b)') OR a = (a ^(a^b')')Program replies True, however the expression is false.
For details see: (*) Hyčko, M., Implications and Equivalences in Orthomodular Lattices, (submitted).
Name | Syntax | Example of usage |
---|---|---|
Evaluating expressions: | ||
Constants: | ||
Zero | 0 | 0 |
Unit | 1 | 1 |
Element with Beran's number | B1(<num>), 1 <= <num> <=96 | B1(13), B1(55) |
Variables: | ||
Element a (1st element of noncompatible pair) | a or x | a |
Element b (2nd element of noncompatible pair) | b or y | b |
Element ci (compatible with each element) | ci, 1<=i<=no_of_comp or c for c1 | c, c1, c5 |
Unary operators: | ||
Complement | expr ' | a', avb', (avb)' |
Binary operators: | ||
Join | expr1 v expr2 or expr1 j expr2 | a'vb' |
Meet | expr1 ^ expr2 or expr1 m expr2 | a'^b |
Skew join - (a ^ b') v b | expr1 sv expr2 or expr1 sj expr2 | a sv b |
Skew meet - (a v b') ^ b | expr1 s^ expr2 or expr1 sm expr2 | a s^ b |
Sasaki projection \varphi_{expr1}(expr2) = expr1 ^ (expr1' v expr2) |
expr1 sp expr2 | a sp b |
Lower commutator | expr1 lc expr2 | a lc b |
Upper commutator | expr1 uc expr2 | a uc b |
Implications: | ||
Classical: expr1' v expr2 | expr1 i0 expr2 | a i0 b |
Sasaki: expr1' v (expr1 ^ expr2) | expr1 i1 expr2 | a i1 b |
Dishkant: expr2 v (expr1' v expr2') | expr1 i2 expr2 | a i2 b |
Kalmbach: ((expr1' ^ expr2) v (expr1' ^ expr2') v (expr1 ^ (expr1' v expr2)) |
expr1 i3 expr2 | a i3 b |
Non-tollens: ((expr1 ^ expr2) v (expr1' ^ expr2)) v ((expr1' v expr2) ^ expr2') |
expr1 i4 expr2 | a i4 b |
Relevance: ((expr1 ^ expr2) v (expr1' ^ expr2)) v (expr1' ^ expr2') |
expr1 i5 expr2 | a i5 b |
Right side of Commutativity relation: (expr1 ^ expr2) v (expr1 ^ expr2') | expr1 oC expr2 | a oC b |
Right side of Dual Commutativity relation: (expr1 v expr2) ^ (expr1 v expr2') | expr1 oD expr2 | a oD b |
Functions: | <fun>(arg1, arg2, ...) | |
B3 | B3(<num>, <arg_a>, <arg_b>), 1 <= <num> <= 96, <arg_a>, <arg_b> - expressions (not relations and if, iff) |
B3(23,a^b, (avb)') |
Relations: | Tests whether expr1 R expr2 | |
Equality | expr1 = expr2 | |
Less than or equal to | expr1 <= expr2 | |
Greater than or equal to | expr1 >= expr2 | |
Commutativity C | expr1 C expr2 | |
AND | rel1 AND rel2 | |
OR | rel1 OR rel2 | DO NOT USE ON THE SIDE OF CONCLUSIONS ! |
If/Iff expressions: | rel1 < '=>' | '<=>' > rel2 | |
if expression | rel1 => rel2 | a<=b=>a C b: a = b => a C b |
if and only if expression | rel1 <=> rel2 | a C b <=> b C a': a C b <=> b C a' |
Operators with same priority use left associativity, i.e. a v b v c = (a v b) v c.
(Character ~ means space)
Operator | RPN | Inverse priority (0=highest) |
---|---|---|
' | ' | 10 |
sp | sp | 40 |
lc | lc | 40 |
uc | uc | 40 |
^ | ^ | 50 |
s^ | s^ | 50 |
v | v | 100 |
sv | sv | 100 |
i0 | i0 | 110 |
i1 | i1 | 110 |
i2 | i2 | 110 |
i3 | i3 | 110 |
i4 | i4 | 110 |
i5 | i5 | 110 |
oC | oC | 120 |
oD | oD | 120 |
= | =~ | 200 |
<= | <= | 200 |
>= | >= | 200 |
C | C | 200 |
AND | A | 250 |
OR! | O | 275 |
=> | if~ | 300 |
<=> | iff | 300 |
Constant | ||
0 | 0 | |
1 | 1 | |
B1(.) | B1 | |
Integer 1<= <n> <=96 | I<0n>~ | <0n> - an extension of one digit number to two digit number with 0 prefix, i.e. 5 ---> 05 |
Variable | ||
a | a | |
x | a | |
b | b | |
y | b | |
c | c1 | |
c1 | c1 | |
c2 | c2 | |
c3 | c3 | |
c4 | c4 | |
c5 | c5 | |
c6 | c6 | |
c7 | c7 | |
c8 | c8 | |
c9 | c9 | |
Function | ||
B3 | B3 |
Ex.1: To check the validity of the Foulis-Holland theorem:
If c is compatible to a and b then a v (b ^ c)=(a v b) ^ ( a v c), a ^ (b v c) = (a ^ b) v (a ^ c),
we need to set number of commutativity elements to 1 (*NEW* or use the Automatic detection, i.e. A) and as an OML expression input: