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

BasicType

BoundedDistributiveLattice

BoundedJoinSemilattice

BoundedLattice

BoundedMeetSemilattice

CoercibleTo OutputForm

DistributiveLattice

JoinSemilattice

Lattice

MeetSemilattice

SetCategory