LatticeJoinOfMeets

logic.spad line 3571 [edit on github]

Infinite Lattice which is distributive. Representation held as join of meets.

/\ : (%, %) -> %

from MeetSemilattice

= : (%, %) -> Boolean

returns true (boolean true) if intuitionisticLogic values are the same. Translates from Intuitionistic Logic to Boolean Logic

T : () -> %

from BoundedMeetSemilattice

\/ : (%, %) -> %

from JoinSemilattice

_|_ : () -> %

from BoundedJoinSemilattice

atom? : % -> Boolean

returns true if this is an atom, that is a leaf node otherwise return false if this is a compound term

coerce : LatticeMeetOfJoins -> %

convert lattice from meet-of-joins to join-of-meets

coerce : % -> LatticeMeetOfJoins

convert lattice from join-of-meets to meet-of-joins

coerce : % -> OutputForm

from CoercibleTo(OutputForm)

deductions : List(%) -> List(%)

assumes ln contains a list of factors which must be true for the whole to be true (such as the list produced by factor). From this deductions attempts to produce a list of other proposition that must also be true by using modus ponens. This is used to determine the returned type when converting ILogic to types by using the Curry-Howard isomorphism.

empty? : % -> Boolean

true if empty

emptyLattice : () -> %

construct an empty lattice

factor : % -> List(%)

splits n into a list of factors which must be true for the whole to be true. This assumes that the top level is already a set of factors separated by /\ otherwise the result will just be a list with one entry: 'n'. This is used when converting ILogic to types by using the Curry-Howard isomorphism.

getChildren : % -> List(%)

returns child nodes if this is a compound term otherwise returns []

join : List(%) -> %

join of set of elements

latex : % -> String

from SetCategory

latticeJoinOfMeets : Union(:(const, Record(val : Symbol)), :(var, Record(str : String))) -> %

construct a lattice with one element

logicF : () -> %

construct false (contradiction): a logical constant.

logicT : () -> %

construct true: a logical constant.

meet : List(%) -> %

meet of set of elements

opType : % -> Symbol

if this is a compound op then opType returns the type of that op: "IMPLY"::Symbol =implies "AND"::Symbol=/\ "OR"::Symbol=\/ "NOT"::Symbol=~ "OTHER"::Symbol=not compound op

redux : % -> %

attempt to simplify terms

toString : % -> String

creates a string representation of this term and its sub-terms

toStringUnwrapped : % -> String

similar to 'toString' but does not put outer compound terms in brackets

value : % -> Symbol

returns: "T"::Symbol = T "F"::Symbol = _|_ "E"::Symbol = error "P"::Symbol = proposition "C"::Symbol = compound Constructs lambda term and bind any variables with the name provided

variable : String -> %

construct a variable

~= : (%, %) -> Boolean

from BasicType

BoundedLattice

CoercibleTo(OutputForm)

DistributiveLattice

BoundedMeetSemilattice

BoundedJoinSemilattice

SetCategory

Lattice

MeetSemilattice

BoundedDistributiveLattice

BasicType

JoinSemilattice