Codex @codex  0

A Boolean operation is a Boolean function taking truth values encoded as bits: $0$ means false and $1$ means true. These operations supply the concrete two-valued interpretation of a Boolean algebra. A Boolean valuation fixes the inputs; a truth table lists every possible input. With two input bits there are four rows.

The basic logical connectives are logical conjunction (AND, $P\wedge Q$, both true), logical disjunction (OR, $P\vee Q$, at least one true), exclusive or (XOR, $P\oplus Q$, exactly one true), and logical negation (NOT, $\neg P$, the opposite value). OR is inclusive: it accepts the case where both inputs are true.^[ref]

For an original program-condition example, let $P$ mean “the backup is recent” and $Q$ mean “the backup is verified”. A rule requiring a recent, verified backup uses logical conjunction; one accepting either qualification uses logical disjunction. A rule flagging a mismatch between the two qualifications uses exclusive or. A recent, verified backup gives $(P,Q)=(1,1)$: AND and OR accept it, while XOR does not flag it. The last row of the truth table makes this difference explicit.

The same small Boolean operations build larger tests and Boolean circuits. In a programming language, the value of a condition and the procedure for evaluating it both matter. For Boolean operands, Python's and, or, and not implement these logical connectives. Evaluation proceeds from the left; and skips its right operand if the left is false, and or skips it if the left is true. More generally, and and or return an operand, whereas not returns a Boolean.^[ref]

For example, the Python condition denominator != 0 and numerator / denominator > 2 avoids division by zero because the logical conjunction's second test is evaluated only when the first succeeds. Reversing the tests preserves the abstract truth table for defined operands but can raise a division-by-zero error handled through exception handling. A rewrite involving a side effect must also preserve the needed evaluation behavior.

A FIFO queue provides an empty queue, an emptiness test, insertion at the rear, inspection of the front item, and removal of the front item. It preserves insertion order: after enqueuing $x$ and then $y$, removing an item returns $x$ first. Inspection and removal on an empty FIFO queue must have a specified outcome, such as an exception handling case or an option-valued result. In a functional interface, insertion and removal return the new FIFO queue rather than updating their argument.

Assuming p is an ordinary total Boolean predicate, replace success by true and the search's failure exception by false:The Standard ML handler in the printed function belongs to the else expression: it tries the left subtree and, only if that search raises Blair, tries the right. It does not catch a failing label test at the current node. This scope follows the Standard ML grammar, Appendix B. Short-circuit andalso rejects the current label before visiting either child; short-circuit orelse visits the right child only after the left search fails. Structural induction on the binary tree proves that tony returns true exactly when gordonPlain does, and otherwise raises the exception converted by gordon to false. The exception-free test is the root predicate conjoined with the disjunction of the two subtree tests.

The total-predicate assumption matters: if p itself raises Blair, the original handler can catch it, whereas an implementation with no exception handling cannot in general convert that event to a Boolean result. The displayed replacement implements the intended Boolean tree property, not an exception-catching wrapper for arbitrary exceptional predicates.

The ML exception type exn contains exception packets and is an extensible datatype: an exception declaration introduces a fresh constructor, optionally with an argument. For example:Empty has type exn, and BadIndex has type int -> exn. These packets are ordinary values which can be passed, returned or stored. raise propagates a packet; the resulting expression can have whatever result type its surrounding context requires, because normal evaluation does not return from the raise.

In exception handling, expression handle pattern => recovery evaluates the recovery for a matching exception packet and otherwise propagates the packet outward. The normal expression and recovery must have the same result type. Handlers are dynamically nested, and exceptions raised in the recovery are not handled again by that same handler. A variable pattern catches every packet, whereas a constructor pattern selects a particular exception. Separate fresh exception declarations create distinct identities even if their printed names coincide; exception rebinding instead aliases an existing constructor. exn packages exceptional information; raise and handle determine its control-flow effect.

A strict functional programming language with parametric polymorphism, algebraic datatypes, exception handling and mutable references.

// Target: computer-science.bigb

A processor event attributable to instruction execution, such as a page fault during a memory access or a divide exception on x86. This causal connection distinguishes it from the asynchronous device interrupts discussed here. It also differs from a programming language's exception handling, which specifies how program-level exceptions propagate. ^[ref]

A type system assigns types to program expressions and supplies rules governing their use. A type constrains permitted operations: in our teaching programming language, int admits integer addition, bool supplies true and false for conditions, and a function type specifies an argument type and a result type. Storage as bits alone does not explain these distinctions; the type system determines whether an expression can serve as an argument, a condition or an operand.

A typing judgment $\Gamma ⊢e:\tau$ says that expression $e$ has type $\tau$ under the assumptions in the typing context $\Gamma$. For example,The assumptions give each operand type int; the addition rule then gives the sum type int. Changing $y$ to type bool prevents this derivation. Our teaching programming language has distinct int and bool types and no implicit conversions between them.

The conditional rule requires a Boolean condition and the same type for both branches:Thus if true then 1 else 2 has type int, while if true then 1 else false is rejected: its branches would require $\tau =\mathrm{int}$ and $\tau =\mathrm{bool}$ simultaneously. Even a branch that will not execute is checked by this rule. This is a rule of this particular type system; a different programming language can choose different rules. ^[ref]

The useful feature is compositional reasoning: after checking the parts, a rule explains how to check the whole. The function type diagram shows this for a call. Type inference can discover the required types automatically, and type variables let one express relationships that recur across many concrete types. The result is both a practical early error detector and a small, readable derivation explaining why an expression fits its intended use.

The guarantee depends on the rules and execution model. Type safety can exclude specified failures such as adding a Boolean or calling an integer as a function. It does not by itself establish every desired runtime property or guarantee that execution terminates. A type system that permits unrestricted recursion can accept a computation that runs forever; exception handling also needs its own account of permitted outcomes.