This is the algebration of poset. A big difference between
this lattice domain and the poset domain is that, in this domain, the
REP holds a single node whereas in poset REP holds the whole poset.

Finite and Infinite Lattices

I would like to implement both finite and Infinite lattices:

Use Bounded versions of Lattice if it has a 'top'/bottom which will be the case for all finite lattices but not infinite lattices since, for finite, we can do a meet/join of all values.


For example consider the integers implemented by:

This constructs a partial order. In this order both meet and join are guaranteed to exist (glb and lub) for any finite set of elements. However top and bottom don't exist (∞ and -∞ are not integers). in other words we can't take a meet or a join of an infinite set of elements.

Another example might be a 'tree', this has a bottom element (root) and joins (including infinite) exist. but meets do not exist and the top element does not exist.

The general case of these examples are recursively defined types.

The following intuitionistic logic code is a sort of 'free' lattice.

Implementation of Intuitionistic Logic

This is infinite in the sense that it is a sort of 'free' lattice.

In OpenAxiom Gaby implemented PropositionalFormula using Kernel like this:

PropositionalFormula(T: SetCategory): Public == Private where
     Rep == Union(T, Kernel %)

I was considering implementing this as discussed on this thread but, if I understand Waldeks reply correctly, there would be little benefit in doing so and it would involve extra complexity of using sparsely documented code like Kernel.

Example of the Use of a Frame in Computer Science

See page here for an example of a frame taken from Vickers section 3.7


The requirements for the existence of of meets and joins correspond to the requirements for the existence of unions and intersections of open sets. Therefore these lattice structures can represent topologies.

  Lattice Open Set
  lat 1 open 1
  lat2 open 2
invalid - every intersection should be an open set: lat open

Topology discussed on this page.

Subset Lattice

This lattice domain implements a subset structure (powerset). The poset equivalent would be a 'containment order'.

One reason for implementing this domain is to investigate the (pseudo)complement.

Here is an test session to show how it works:

     -- first setup some variables
     SL := SubsetLattice(NNI,[1,2,3])
 (1)  SubsetLattice(NonNegativeInteger,[1,2,3])
     Type: Type
     a := subsetLattice([1])$SL
 (2)  [1]
     Type: SubsetLattice(NonNegativeInteger,[1,2,3])
     b := subsetLattice([2])$SL
 (3)  [2]
     Type: SubsetLattice(NonNegativeInteger,[1,2,3])
     -- test meet and join
 (4)  [1,2]
     Type: SubsetLattice(NonNegativeInteger,[1,2,3])
 (5)  []
     Type: SubsetLattice(NonNegativeInteger,[1,2,3])
     -- test complement
 (6)  [2,3]
     Type: SubsetLattice(NonNegativeInteger,[1,2,3])
 (7)  [3]
     Type: SubsetLattice(NonNegativeInteger,[1,2,3])

Infinite (unbounded) Lattices

Arbitrary vs. Finite Conjunction and Disjunctions

This structure makes a distinction between arbitrary and finite conjunction/disjunctions.
This is related to the convergence of a sequence (Hausdorff Umgebungsaxiome).

For example: a sequence of ever-smaller open intervals around zero: (-1,1), (-1/2,1/2), (-1/3,1/3), ...

For unions:

For intersections:

We cannot determine if arbitrary (infinite) frames are equal because, however many terms of two frames that start with the same values we have, they might be still be extended with different values. We can never check the complete frame because we cannot hold an infinite structure in a finite computer.

Algebra of Frames

Translating this into lattice algebra:
If A and B are semi-decidable then:

See [5]

Distributive Lattices

Not every lattice is distributive but those that are have some interesting properties which can be investigated by using these domains.

If the lattice is distributive then we can take advantage of this and make the representation more efficient by representing it as either:


(a\/b\/...) /\ (c\/d\/...) /\ ...


(a/\b/\...) \/ (c/\d/\...) \/ ...

So the representation is a list of lists like this:

Rep := List List Union(_
     const : Record(val : Symbol), _
     var : Record(str : String) _

For a finite lattice then:
if meet is distributive over join, then join is also distributive over meet.
if join is also distributive over meet, then meet is distributive over join.

We can therefore always convert between join-of-meets and meet-of-joins by 'multiplying' out the terms and applying the idempotence + absorption axioms.

We therefore only need one of these domains to represent a distributive lattice structure. However I have provided both to allow conversions between the two types to be provided.

I look at this like a polynomial for lattices and these conversions are like solving a polynomial.

Here is an test session to show how it works:

-- first setup some variables
     MOJ := LatticeMeetOfJoins
(1)  LatticeMeetOfJoins
                                              Type: Type
     a := variable("a")$MOJ
(2)  ("a")
                         Type: LatticeMeetOfJoins
     b := variable("b")$MOJ
(3)  ("b")
                         Type: LatticeMeetOfJoins
     c := variable("c")$MOJ
(4)  ("c")
                           Type: LatticeMeetOfJoins
     d := variable("d")$MOJ
(5)  ("d")
                           Type: LatticeMeetOfJoins
     -- test 'and'
     land := a /\ b
(6)  ("a")/\("b")
                           Type: LatticeMeetOfJoins
     -- opposite
     landOp := land::LatticeJoinOfMeets
(7)  ("a"/\"b")
                           Type: LatticeJoinOfMeets
     -- test or
     lor := a \/ b
(8)  ("a"\/"b")
                           Type: LatticeMeetOfJoins
     -- opposite
     lorOp := lor::LatticeJoinOfMeets
(9)  ("a")\/("b")
                             Type: LatticeJoinOfMeets
     -- test idempotence (should return 'a')
     a /\ a
(10)  ("a")
                             Type: LatticeMeetOfJoins
     a \/ a
(11)  ("a")
                             Type: LatticeMeetOfJoins
     -- test absorption (should return 'a')
(12)  ("a")
                             Type: LatticeMeetOfJoins
(13)  ("a")
                                      Type: LatticeMeetOfJoins
     -- test composite contructions
     landor := land \/ c
(14)  ("a"\/"c")/\("b"\/"c")
                                      Type: LatticeMeetOfJoins
     landorOp := landor::LatticeJoinOfMeets
(15)  ("a"/\"b")\/("c")
                                      Type: LatticeJoinOfMeets
     landorOpOp := landorOp::LatticeMeetOfJoins
(16)  ("a"\/"c")/\("b"\/"c")
                                     Type: LatticeMeetOfJoins
     landorand := landor /\ d
(17)  ("a"\/"c")/\("b"\/"c")/\("d")
                                   Type: LatticeMeetOfJoins
     landorandOp := landorand::LatticeJoinOfMeets
(18)  ("a"/\"b"/\"d")\/("c"/\"d")
                                     Type: LatticeJoinOfMeets
     landorandOpOp := landorandOp::LatticeMeetOfJoins
(19)  ("a"\/"c")/\("b"\/"c")/\("d")
                                      Type: LatticeMeetOfJoins


[5] Blog about semi-decidable logic

metadata block
see also:
Correspondence about this page

Book Shop - Further reading.

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.

flag flag flag flag flag flag Axiom Volume 1: Tutorial. Documentation is freely availible from:


This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2017 Martin John Baker - All rights reserved - privacy policy.