Skip to content

Instantly share code, notes, and snippets.

# msakai/DistributiveLattice.als

Created July 27, 2011 00:04
Alloy model that demonstrate every non-distributive lattice contains one of the two particular lattices as a subpseudolattice.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 sig L { join, meet : L -> one L } one sig top, bot in L {} fact { all x, y, z : L { -- commutativity x.join[y] = y.join[x] x.meet[y] = y.meet[x] -- associativity x.join[y].join[z] = x.join[y.join[z]] x.meet[y].meet[z] = x.meet[y.meet[z]] -- unit laws x.meet[top] = x x.join[bot] = x -- idempotence x.join[x] = x x.meet[x] = x -- absorption x.meet[x.join[y]] = x x.join[x.meet[y]] = x } } pred show {} run show for 5 L pred le[x, y : L] { x.join[y]=y } pred le'[x, y : L] { x.meet[y]=x } assert le_welldefined { all x, y : L | le[x,y] <=> le'[x,y] } check le_welldefined for 8 L assert le_poset { -- reflexivity all x : L | le[x,x] -- transitivity all x, y, z : L | le[x,y] and le[y,z] => le[x,z] -- antisymmetry all x, y : L | le[x,y] and le[y,x] => x=y } check le_poset for 8 L assert le_top { all x : L | le[x,top] } check le_top for 8 L assert le_bot { all x : L | le[bot,x] } check le_bot for 8 L pred distributivity { all x, y, z : L | x.meet[y.join[z]] = x.meet[y].join[x.meet[z]] } run distributivity for 5 L pred distributivity' { all x, y, z : L | x.join[y.meet[z]] = x.join[y].meet[x.join[z]] } assert dualDistributivityHolds{ distributivity => distributivity' } check dualDistributivityHolds for 8 L pred p1 { some disj a,b,c,d,e : L { a = a.join[b] d = a.join[c] d = b.join[c] e = a.meet[c] e = b.meet[c] } } pred p2 { some disj a,b,c,d,e : L { d = a.join[b] d = a.join[c] d = b.join[c] e = a.meet[b] e = a.meet[c] e = b.meet[c] } } assert nondistributiveSubPseudoLattice { !distributivity <=> (p1 || p2) } check nondistributiveSubPseudoLattice for 8 L
to join this conversation on GitHub. Already have an account? Sign in to comment