FunctionaL City’s algebraic infrastructure has advanced significantly. The original collapse to concrete logic gave us a way to reduce lifted unions into concrete sets. Since then, constructors have been refactored, infinite sets now use rule dictionaries, and implication logic is embedded directly into the constructors. This post documents those changes and explains why union is the next piece to revisit.
Earlier, evaluating infinite sets risked runaway computation. The solution was to introduce bounded evaluation: comparisons are only made up to a fixed equivalenceDepth. This prevents uncontrolled expansion while still allowing symbolic exploration.
On top of that, every operation now classifies its result as:
This classification is attached to results along with provenance notes, so remixers can see not just what happened, but why.
Two constructors now define how sets are built:
let naturalNumbersSpec : CivicSetRule<int> =
{ Filter = fun n -> n >= 0;
Generator = fun i -> i;
Formula = Some natFormula;
Provenance = natProvenance;
Max = None;
Min = Some 0;
Compare = Some compare
Metadata = {Cardinality = Some Aleph0;
Countability = Some Countable;
OrderType = Some TotalOrder}
Note = "ℕ, the set of natural numbers ≥ 0, originates from Giuseppe Peano's 1889 axioms, ..."
}
// Create a dictionary for infinite integer sets.
let intRules : CivicSetRuleDictionary<int> = (Map.ofList [("\u2115", naturalNumbersSpec);("\u2124", integersSpec)])
// Cast defaultSet to a concrete type
let defaultS = CivicSetConstructors.defaultSet :> ICivicSet<int>
let Odds = CivicSetConstructors.finiteSet "Odds" [1;3;5;7;9] None (Some naturalNumbersSpec)
let naturalNumbers = CivicSetConstructors.infiniteSet intRules "\u2115" equivalenceDepth |> Option.defaultValue defaultS
This separation makes it clear: finite sets are concrete, infinite sets are symbolic. Both constructors embed implication and difference logic directly, so reasoning is part of the object itself.
Set difference was introduced as a core operation, and implication checks now use it directly. Instead of naïvely enumerating infinite sets, differences are bounded and classified.
This ensures infinite sets are narratable without risking runaway evaluation. Each result carries provenance notes, counterexamples, and cardinality checks.
Implication: ℕ ⇒ ℤ
Success: true
Message: "All members of ℕ are contained in ℤ — implication holds"
Provenance: ℕ ⊆ ℤ within bounded depth
Implication: ℤ ⇒ ℕ
Success: false
Message: "Implication fails — ℤ contains members not in ℕ"
Counterexamples: [-1; -2; -3; -4; ...]
Implication: setA ⇒ setB
Success: false
Message: "Implication fails with 2 counterexample(s) found"
Counterexamples: [2; 4]
Set Difference: ℤ \ ℕ
Success: true
Message: "Result (ℤ \ ℕℤ) has ℵ₀ cardinality — may be lazily enumerable or infinite"
Elements (sample): [-1; -2; -3; -4; -5; ...]
Set Difference: ℕ \ Oddsℕ (Odds is a finite set)
Success: true
Message: "Result (ℕ \ Oddsℕ) has ℵ₀ cardinality — may be lazily enumerable or infinite"
Elements (sample): [0; 2; 4; 6; 8; 10; 11; 12; 13; 14]
These outputs show how implication and difference now produce diagnostic results with provenance notes, counterexamples, and cardinality checks. Infinite sets are no longer dangerous black boxes — they are bounded, classified, and inspectable.
Union was originally designed before several key advances in the infrastructure:
With the new architecture in place, union must evolve to align with these changes.
Integrate rule-based infinite sets
Unions should carry symbolic formulas and registry provenance, not just lifted wrappers.
Narrate compatibility checks
Collapse should emit overlays when provenance differs or a comparer is missing, so remixers can see why a union is lawful or rejected.
Leverage implication + difference
Union should scaffold distributivity and absorption laws, using the same bounded evaluation and classification strategy as difference and implication.
Support mixed unions
Finite ∪ infinite unions should produce symbolic overlays, preserving lineage and computability notes.
By revisiting union with these principles, FunctionaL City ensures that set theory operations remain narratable, remixable, and practical for both coders and remixers.
testUnionCompatibility
A narratable helper to inspect union eligibility before execution.
It will check provenance, comparer presence, and cardinality, and emit overlays explaining why a union is lawful or rejected.
collapseLiftedToConcrete with Infinite set support.
An extended ordinance allowing symbolic collapse with overlays.
This will support infinite unions by tagging results with provenance such as "union/infinite" and attaching diagnostics about computability.
Glossary Crosslinks
New entries for:
By codifying these ordinances ensures that union joins is a fully narratable and remix‑safe operation.
City Limits
Primitives ordinance book.
First Order Logic ordinance book.
Civic Set ordinance book.
Keep an eye out for future editions of Message from the Mayor as the city grows and random musings develop along the way. In the meantime, keep an eye on the BlogDistrict README.md for updates.
With this amendment ratified and the roadmap charted, FunctionaL City continues its march toward a narratable, remixable civic future.
Signed,
FrankL
Mayor and City Engineer of FunctionaL City