Door de zeer eenvoudige overeenkomst van de bit-AND met de haak-OR leent het binair model van het haakformalisme zich tot een zeer gemakkelijke modellering van invarianten, aangezien invarianten gegeven worden door nevenschikking. We demonstreren dat met het meest eenvoudige model van invariantie en zijn vertaling in vier bits.
|
|
a |
1010 |
|
|
ab |
1000 |
|
|
a<b> |
0010 |
|
|
<> |
0000 |
|
|
Het patroon dat hier naar boven komt wordt duidelijk als we de bits die in de vier punten gemeenschappelijk zijn door een don't care vervangen en dan ook de vertaling als waardetoekenning van een welgevormde haakuitdrukking, merk op dat a↔<<>> inderdaad codeert voor een deeltralie:
|
|
a↔<<>> |
1x1x |
|
|
a↔<<>> |
1x0x |
|
|
a↔<<>> |
0x1x |
|
|
a↔<<>> |
0x0x |
|
|
De structuur wordt maar door twee bits gecodeerd, de twee overige bits zijn invariant en het is juist dit dat door een waardetoekenning gemodelleerd wordt.
Dit maakt ook duidelijk dat het aantal don't cares geen rol speelt voor de gemodelleerde structuur (in dit geval een één onderscheiding universum), wat we bijvoorbeeld kunnen uitdrukken in de volgende tralie:
|
|
a↔<<>> |
1x1x.xxxx |
|
|
a↔<<>> |
1x0x.xxxx |
|
|
a↔<<>> |
0x1x.xxxx |
|
|
a↔<<>> |
0x0x.xxxx |
|
|
De invariant a kunnen we dus interpreteren als de intensiteit van don't cares wanneer a gebeurt (een waarde heeft niet verschillend van <<>>).
De invariantie is altijd ten opzichte van een tralie en dat demonstreren we met de volgende tralie van acht punten in het twee onderscheidingen universum die geen voorwaarden stelt wat betreft collaps (er zijn geen gemeenschappelijke bits) en stellen dat voor met haakuitdrukking en bitstring. We kiezen voor deze tralie omdat deze te vinden is in elke tralie vanaf twee onderscheidingen. We doen dat op een didactische manier door in een paar stappen de eerst gemaakte veronderstellingen los te laten.
<<>> |
1111 |
|
|
|
|
b |
1100 |
<ab> |
0111 |
<b<a>>∼(a⊗<<>>)b |
1011 |
b<a>∼(<b>⊗<>)b |
0100 |
ab |
1000 |
<b> |
0011 |
<> |
0000 |
|
|
|
|
We voegen nu een invariant toe, namelijk de derde onderscheiding c:
c<<>> |
1111.0000 |
|
|
|
|
cb |
1100.0000 |
c<ab> |
0111.0000 |
c<b<a>>∼c(a⊗<<>>)b |
1011.0000 |
cb<a>∼c(<b>⊗<>)b |
0100.0000 |
cab |
1000.0000 |
c<b> |
0011.0000 |
c<> |
0000.0000 |
|
|
|
|
De tralie blijft behouden, maar er worden dus bits nevengeschikt overal op dezelfde plaats in de string. Dat is dus een niet gecollapste deeltralie in een grotere tralie. De nevengeschikte bits zijn dus bits die gedurende een heel proces die enkel zou ageren op de andere bits dezelfde waarde blijven behouden. Elk van de 8 punten is een join (symbool ∨) van c met zichzelf, dus c is invariant.
Als volgende uitbreiding kunnen we dus zien dat de bits die de tralie relatie tonen onafhankelijk zijn van de positie in de grotere bitstring zoals bijvoorbeeld voor de invariant <a<<b>c>><<a>c<b>>, en we kiezen uit de algemene tabel van de punten uit een drie onderscheidingen universum hierbij een vorm uitgedrukt als creatief product voor toevoeging van a (wat uiteraard een volledig willekeurige keuze is).
<a<<b>c>><<a>c<b>> |
0110.0101 |
|
|
|
|
<a<<b>c>><<a><cb>> |
0110.0000 |
<a<<b>c>><<a>c> |
0010.0101 |
<a<<>>><<a>c<b>> |
0100.0101 |
<a<<b>c>><<a><<>>> |
0010.0000 |
<a<<>>><<a><bc>> |
0100.0000 |
<a<<>>><<a>c> |
0000.0101 |
<a<<>>><<a><<>>> |
0000.0000 |
|
|
|
|
In bitstring is het snel te controleren dat
(0110.0101)∨(1111.1111)=(0110.0101)
(0110.0101)∨(0110.0000)=(0110.0000)
(0110.0101)∨(0010.0101)=(0010.0101)
enz...
Als we nu de volgende tabel opbouwen dan is duidelijk dat dit isomorf is met de tralie die vanuit de relatie van relevantie kan opgebouwd worden, wat betekent dat in haakuitdrukking een waarde toegekend wordt aan de invariant.
<a<<b>c>><<a>c<b>>↔<<>> |
x11x.x1x1 |
|
|
|
|
<a<<b>c>><<a>c<b>>↔<<>> |
x11x.x0x0 |
<a<<b>c>><<a>c<b>>↔<<>> |
x01x.x1x1 |
<a<<b>c>><<a>c<b>>↔<<>> |
x10x.x1x1 |
<a<<b>c>><<a>c<b>>↔<<>> |
x01x.x0x0 |
<a<<b>c>><<a>c<b>>↔<<>> |
x10x.x0x0 |
<a<<b>c>><<a>c<b>>↔<<>> |
x00x.x1x1 |
<a<<b>c>><<a>c<b>>↔<<>> |
x00x.x0x0 |
|
|
|
|
We kunnen in een volgende uitbreiding ook het infimum veranderen. Tot nu toe hebben we de 0-bit genomen als invariant voor elke positie, en zo kwamen we uit op het infimum <>, maar dit is geen noodzakelijkheid. In de volgende tabel gebruiken we één 1-bit en drie 0-bits waarbij we de posities van de invarianten in de vorige tabel ongemoeid laten. Nu ook weer kiezen we eerst de bitstring en kiezen dan een vertaling in haakuitdrukking uit het drie onderscheidingen universum met a als toegevoegde onderscheiding:
<a<c<b>>><<a><>> |
0111.0101 |
|
|
|
|
<a<<b>c>><<a><c>> |
0111.0000 |
<a<<b>c>><<a>bc> |
0011.0101 |
<a<<>>><<a><>> |
0101.0101 |
<a<<b>c>><<a><<b>c>> |
0011.0000 |
<a<<>>><<a><c>> |
0101.0000 |
<a<<>>><<a>bc> |
0001.0101 |
<a<<>>><<a><<b>c>> |
0001.0000 |
|
|
|
|
Dit maakt duidelijk dat we twee invarianten onderscheiden: een invariant voor de disjunctie en een invariant voor de conjunctie. Het supremum is invariant voor een join met elk punt, het infimum is invariant voor een meet met elk punt.