finite-sets-logic

The finite-sets-logic worked example.

Run it from sema/:

sema check examples/finite-sets-logic
SEMA_STRICT=1 sema run examples/finite-sets-logic
sema assure examples/finite-sets-logic --grade silver

Source

src/main.sema

"""Bounded exact finite sets and explicit three-valued logic.

`FiniteSet` is immutable, extensional, and never inferred from a scalar. Sets
hold at most 4,096 canonical finite elements; `power_set` accepts at most 12
inputs, and indexed intersection of an empty family is `UnknownUniverse`.
`Truth.unknown(reason)` has no implicit boolean conversion: resolve it with the
strong-Kleene `logical_*` operations or compare it explicitly.
"""

assure silver

def classify(value: int) -> Truth !{}:
    if value == 2:
        return Truth.unknown("classification for 2 is pending")
    return Truth.true

test "constructors and algebra are exact and canonical":
    left = FiniteSet(3, 1, 2, 2)
    right = set([2, 4])
    check left == {1, 2, 3}
    check union(left, right) == {1, 2, 3, 4}
    check intersection(left, right) == {2}
    check set_difference(left, right) == {1, 3}
    check symmetric_difference(left, right) == {1, 3, 4}

test "bounded derived sets stay explicit":
    check cartesian_product({1, 2}, {3}) == {(1, 3), (2, 3)}
    check len(power_set({1, 2, 3})) == 8
    check indexed_union([{1, 2}, {2, 3}]) == {1, 2, 3}
    check indexed_intersection([{1, 2}, {2, 3}]) == {2}

test "unknown quantifier results are never false by coercion":
    verdict = forall({1, 2, 3}, classify)
    check verdict == Truth.unknown("classification for 2 is pending")
    check logical_and(verdict, false) == Truth.false
    check logical_or(verdict, true) == Truth.true

def main() -> str !{observe.record}:
    values = {1, 2, 3}
    verdict = forall(values, classify)
    ensure verdict == Truth.unknown("classification for 2 is pending")
    log.info("finite logic", values=values, verdict=verdict)
    return "bounded finite-set algebra and explicit Unknown verified"

Reflected API

main

Bounded exact finite sets and explicit three-valued logic.

FiniteSet is immutable, extensional, and never inferred from a scalar. Sets hold at most 4,096 canonical finite elements; power_set accepts at most 12 inputs, and indexed intersection of an empty family is UnknownUniverse. Truth.unknown(reason) has no implicit boolean conversion: resolve it with the strong-Kleene logical_* operations or compare it explicitly.

def classify

def classify(value: int) -> Truth !{}

Parameters

name	type
value	int

Returns Truth

Effects !{}

def main

def main() -> str !{observe.record}

Returns str

Effects !{observe.record}