LatticeJoinOfMeets¶

logic.spad line 3575 [edit on github]

parse result includes term returned and new index

/\: (%, %) -> %: from MeetSemilattice

=: (%, %) -> Boolean: returns true (boolean true) if intuitionisticLogic values are the same. Translates from Intuitionistic Logic to Boolean Logic

\/: (%, %) -> %: from JoinSemilattice

_|_: %: from BoundedJoinSemilattice

~=: (%, %) -> Boolean: from BasicType

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 join-of-meets to meet-of-joins
coerce: % -> OutputForm: from CoercibleTo OutputForm

coerce: LatticeMeetOfJoins -> %: convert lattice from meet-of-joins to join-of-meets

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

T: %: from BoundedMeetSemilattice

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

BoundedDistributiveLattice

BoundedJoinSemilattice

BoundedMeetSemilattice

CoercibleTo OutputForm

DistributiveLattice

JoinSemilattice

MeetSemilattice