The Avail Programming Language

boolean ≝ {true, false}ᵀ

type lattice focused on boolean

Rather than being a specialized type, boolean is simply the name given to the enumeration of the special atoms true and false: {true, false}ᵀ. These atoms are defined and exported by the virtual machine for use by programmers. Every primitive interrogative method, such as "_=_" or "_≤_", uses classical (Boolean) bivalence, and every stable primitive interrogative obeys the three classical (Aristotelian) laws of thought.

Bivalent logic assigns either true or false as the unique truth value of every proposition. A primitive interrogative method is stable iff it reliably answers either true or false for a given set of arguments.

The classical laws of thought are:

  • The law of identity, that every proposition P implies itself: P → P. For every stable primitive interrogative method "prim_,_", then ∀A,B : (prim A, B = prim A, B) = true.
  • The law of noncontradiction, that both a proposition P and its negation ¬P are not mutually true: ¬(P ∧ ¬P). For every stable primitive interrogative method "prim_,_", then ∀A,B : (prim A, B ∧ ¬prim A, B) = false.
  • The law of excluded middle, that either a proposition P or its negation ¬P is uniquely true: P ∨ ¬P. For every primitive interrogative method "prim_,_", then ∀A,B : ((prim A, B = true) ∨ (prim A, B = false)) = true.

Remember that values may be instances of many types. This means that Avail directly supports other logical systems, such as Kleene's three-valued logic of indeterminacy, whose truth values are true, false, and unknown. Assuming the introduction of an atom to represent unknown, then kleenean ≝ {true, false, unknown}ᵀ. Clearly kleenean is a supertype of boolean, since {true, false, unknown}ᵀ ⊇ {true, false}ᵀ. New logical operations could be written in terms of kleenean, and preexisting logical operations defined to accept booleans would automatically become specializations of these more general operations defined to accept kleeneans.

/* A proof that boolean is merely a type comprising only true and false: */ Assert: boolean = {true, false}ᵀ; /* Introduce an atom named "unknown" into the current module's context. */ "unknown" is a new atom; /* Define the "kleenean" type; boolean ∪ (unknown's type) would also have * worked. */ kleenean ::= {true, false, unknown}ᵀ; Assert: boolean ⊆ kleenean; /* Define a method "truth index of_" that accepts a Kleenean truth value and * answers an appropriate index into one of the truth tables below. */ Abstract method "truth index of_" is [kleenean]→[1..3]; Method "truth index of_" is [p : true's type | 1]; Method "truth index of_" is [p : unknown's type | 2]; Method "truth index of_" is [p : false's type | 3]; /* * In each of the truth tables, whether the subscript applies to a row or a * column, a subscript of 1 means "true", 2 means "unknown", and 3 means * "false". */ notTable ::= <false, unknown, true>; andTable ::= < <true, unknown, false>, <unknown, unknown, false>, <false, false, false> >; orTable ::= < <true, true, true>, <true, unknown, unknown>, <true, unknown, false> >; /* * And here are the logical operators themselves. */ /* Kleenean NOT. */ Method "¬_" is [ a : kleenean | notTable[truth index of a] ] : kleenean; /* Kleenean AND. */ Method "_∧_" is [ a : kleenean, b : kleenean | andTable[truth index of a][truth index of b] ] : kleenean; /* Kleenean OR. */ Method "_∨_" is [ a : kleenean, b : kleenean | orTable[truth index of a][truth index of b] ] : kleenean; /* The first assertion invokes the boolean versions of "¬_" and "_∧_", but the * second one invokes the kleenean version of "_∨_". So booleans and kleeneans * interoperate nicely. */ p : boolean := true; q : kleenean := unknown; Assert: (p ∧ false) = false; Assert: (p ∨ q) = true;
atom | Return to Type System | object