From e9e0a462ac9f928f9984404f827927b4241729c6 Mon Sep 17 00:00:00 2001 From: Hassan Abedi Date: Wed, 11 Mar 2026 10:24:56 +0100 Subject: [PATCH] Add geolog examples to the project --- examples/geolog/README.md | 470 ++++++++++++++++++ examples/geolog/category.geolog | 86 ++++ .../geolog/field_projection_chase_test.geolog | 27 + examples/geolog/field_projection_test.geolog | 12 + examples/geolog/graph.geolog | 79 +++ examples/geolog/iso_instance_test.geolog | 29 ++ examples/geolog/iso_theory_test.geolog | 9 + examples/geolog/monoid.geolog | 78 +++ examples/geolog/nested_instance_test.geolog | 33 ++ examples/geolog/petri_net.geolog | 135 +++++ examples/geolog/petri_net_full.geolog | 195 ++++++++ examples/geolog/petri_net_showcase.geolog | 345 +++++++++++++ examples/geolog/petri_net_solution.geolog | 188 +++++++ examples/geolog/petri_reachability.geolog | 164 ++++++ .../petri_reachability_full_vision.geolog | 72 +++ .../geolog/petri_reachability_vision.geolog | 94 ++++ examples/geolog/petri_trace_axioms.geolog | 66 +++ .../geolog/petri_trace_coverage_test.geolog | 36 ++ .../geolog/petri_trace_full_vision.geolog | 57 +++ examples/geolog/petri_trace_test.geolog | 58 +++ examples/geolog/preorder.geolog | 42 ++ .../product_codomain_equality_test.geolog | 23 + examples/geolog/product_codomain_test.geolog | 51 ++ .../geolog/record_existential_test.geolog | 18 + examples/geolog/record_in_axiom_test.geolog | 12 + .../geolog/record_premise_chase_test.geolog | 23 + examples/geolog/relalg_simple.geolog | 130 +++++ examples/geolog/solver_demo.geolog | 132 +++++ examples/geolog/sort_param_simple.geolog | 31 ++ examples/geolog/todo_list.geolog | 44 ++ examples/geolog/transitive_closure.geolog | 77 +++ 31 files changed, 2816 insertions(+) create mode 100644 examples/geolog/README.md create mode 100644 examples/geolog/category.geolog create mode 100644 examples/geolog/field_projection_chase_test.geolog create mode 100644 examples/geolog/field_projection_test.geolog create mode 100644 examples/geolog/graph.geolog create mode 100644 examples/geolog/iso_instance_test.geolog create mode 100644 examples/geolog/iso_theory_test.geolog create mode 100644 examples/geolog/monoid.geolog create mode 100644 examples/geolog/nested_instance_test.geolog create mode 100644 examples/geolog/petri_net.geolog create mode 100644 examples/geolog/petri_net_full.geolog create mode 100644 examples/geolog/petri_net_showcase.geolog create mode 100644 examples/geolog/petri_net_solution.geolog create mode 100644 examples/geolog/petri_reachability.geolog create mode 100644 examples/geolog/petri_reachability_full_vision.geolog create mode 100644 examples/geolog/petri_reachability_vision.geolog create mode 100644 examples/geolog/petri_trace_axioms.geolog create mode 100644 examples/geolog/petri_trace_coverage_test.geolog create mode 100644 examples/geolog/petri_trace_full_vision.geolog create mode 100644 examples/geolog/petri_trace_test.geolog create mode 100644 examples/geolog/preorder.geolog create mode 100644 examples/geolog/product_codomain_equality_test.geolog create mode 100644 examples/geolog/product_codomain_test.geolog create mode 100644 examples/geolog/record_existential_test.geolog create mode 100644 examples/geolog/record_in_axiom_test.geolog create mode 100644 examples/geolog/record_premise_chase_test.geolog create mode 100644 examples/geolog/relalg_simple.geolog create mode 100644 examples/geolog/solver_demo.geolog create mode 100644 examples/geolog/sort_param_simple.geolog create mode 100644 examples/geolog/todo_list.geolog create mode 100644 examples/geolog/transitive_closure.geolog diff --git a/examples/geolog/README.md b/examples/geolog/README.md new file mode 100644 index 0000000..04a0b85 --- /dev/null +++ b/examples/geolog/README.md @@ -0,0 +1,470 @@ +# Geolog DSL Structure + +This directory contains example `.geolog` files that use a richer DSL than the +minimal `.chase` script language in `examples/scripts/`. + +This README summarizes the Geolog DSL structure as it appears in the examples in +this directory. It should be read as a practical, example-driven reference, not +as a formal or complete language specification. + +## At a Glance + +- Top-level declarations are `theory` and `instance`. +- The main kind of type is `Sort`. +- Symbols can denote sorts, constants, functions, predicates, or nested + instances. +- Axioms use sequent-style syntax: `premise |- conclusion`. +- Instance bodies can be plain literals (`= { ... }`) or chase blocks + (`= chase { ... }`). +- Function application is postfix, and qualified names use `/`. + +## Informal File Shape + +```text +file := { comment | theory_decl | instance_decl } + +comment := // ... + +theory_decl := + theory theory_params? Name { + theory_item* + } + +instance_decl := + instance Name : theory_app = { + instance_item* + } + + | instance Name : theory_app = chase { + instance_item* + } +``` + +In practice, a file is usually a sequence of theory declarations followed by one +or more example instances. + +## Top-Level Declarations + +### `theory` + +A theory introduces sorts, symbols, and axioms. + +```text +theory Graph { + V : Sort; + Edge : [src: V, tgt: V] -> Prop; +} +``` + +Theories may also be parameterized. + +```text +theory (X : Sort) (Y : Sort) Iso { + fwd : X -> Y; + bwd : Y -> X; +} + +theory (N : PetriNet instance) Marking { + token : Sort; + token/of : token -> N/P; +} +``` + +Observed parameter forms: + +- sort parameters: `(X : Sort)` +- instance parameters: `(N : PetriNet instance)` +- dependent instance parameters: `(RP : N ReachabilityProblem instance)` + +### `instance` + +An instance provides concrete elements and assignments for a theory. + +```text +instance Triangle : Graph = { + A : V; + B : V; + C : V; +} +``` + +Instances may target parameterized theories by writing the arguments before the +theory name. + +```text +instance MyMap : MyBase Map = { ... } +instance solution0 : ExampleNet problem0 Solution = { ... } +instance AB_Iso : As/a Bs/b Iso = { ... } +``` + +## Theory Body Items + +The examples show the following declaration forms inside a theory body. + +### Sort declarations + +```text +V : Sort; +E : Sort; +``` + +This introduces carrier sorts. + +### Constants or distinguished elements + +```text +elem : X; +``` + +This introduces a named element of an existing sort. + +### Functions + +```text +src : E -> V; +fwd : X -> Y; +token/of : token -> N/P; +``` + +Names may contain `/`, which is used heavily for structured or qualified names. + +### Predicates and relations + +Unary predicates: + +```text +completed : Item -> Prop; +``` + +Record-shaped predicates: + +```text +Edge : [src: V, tgt: V] -> Prop; +depends : [item: Item, on: Item] -> Prop; +``` + +### Product-valued functions + +Functions may return record-shaped values. + +```text +pair_of : A -> [left: B, right: C]; +W/src : W -> [firing: F, arc: N/out]; +``` + +### Nested instance slots + +Theories can contain fields whose values are themselves instances. + +```text +initial_marking : N Marking instance; +trace : N Trace instance; +initial_iso : (trace/input_terminal) (RP/initial_marking/token) Iso instance; +``` + +### Axioms + +Axioms use a sequent-like form. + +```text +ax/trans : forall x, y, z : V. + [src: x, tgt: y] Path, [src: y, tgt: z] Path |- [src: x, tgt: z] Path; +``` + +An axiom declaration has the observed structure: + +```text +name : forall binders. premise |- conclusion; +``` + +## Formula and Term Syntax + +The examples use the following building blocks inside axioms and assignments. + +### Quantifiers + +Universal binders appear after `forall`. + +```text +forall x : X, y : Y. +``` + +Existentials appear directly inside conclusions or disjuncts. + +```text +exists r : R. r R/data = [x: a, y: b] +exists w : W. w W/src_firing = f, w W/src_arc = arc +``` + +### Sequents + +The central connective is `|-`, separating premise from conclusion. + +```text +premise1, premise2 |- conclusion1, conclusion2; +``` + +In the examples: + +- commas act as conjunctions +- the left side is the premise +- the right side is the conclusion + +### Equality + +Equality is used for ordinary values and compound values. + +```text +ab src = A +r R/data = [x: a, y: b] +x fwd bwd = x +``` + +### Truth constants + +```text +|- true; +|- false; +``` + +### Disjunction + +Disjunction is written as `\/`. + +```text +[item: x, on: y] depends |- x blocked \/ y completed; +``` + +### Predicate atoms + +Unary predicate atoms: + +```text +x blocked +y completed +``` + +Record-shaped predicate atoms: + +```text +[src: x, tgt: y] Edge +[a: x, f: i] id +``` + +### Postfix application + +Function application is postfix and can be chained. + +```text +e src +x id +x fwd bwd +w W/src_arc N/out/tgt +``` + +This is one of the most distinctive traits of the DSL. + +### Qualified paths + +The slash `/` is used for qualification and nested access. + +Observed examples include: + +```text +R/data +N/P +N/out/src +trace/input_terminal +RP/initial_marking/token +ExampleNet/A +``` + +### Record literals + +Records are written with brackets and named fields. + +```text +[x: a, y: b] +[firing: f, arc: arc] +``` + +The examples also show positional shorthand for record arguments when the field +order is known: + +```text +[e, e] mul = e; +[cook_dinner, on: buy_groceries] depends; +``` + +### Field projection + +Record-valued terms support field projection. + +```text +r R/data .x = a +``` + +## Instance Body Items + +The examples show the following forms inside instance bodies. + +### Element declarations + +```text +a : V; +tok : token; +ab : T; +``` + +### Function assignments + +```text +ab src = A; +tok token/of = ExampleNet/A; +a1 map = MyBase/b1; +``` + +### Predicate facts + +Unary facts: + +```text +buy_groceries completed; +``` + +Record-shaped facts: + +```text +[src: a, tgt: b] Edge; +[item: x, on: y] depends; +``` + +### Product-valued assignments + +```text +a1 pair_of = [left: b1, right: c1]; +ot output_terminal/src = [firing: f1, arc: SimpleNet/arc_out]; +``` + +### Nested instance literals + +Instance-valued fields can be assigned inline blocks. + +```text +initial_marking = { + tok : token; + tok token/of = ExampleNet/A; +}; +``` + +## `= { ... }` vs `= chase { ... }` + +The examples consistently use two instance forms. + +### Plain instance + +```text +instance Triangle : Graph = { + ... +} +``` + +This gives a direct structure with only the explicitly listed elements and +assignments. + +### Chase instance + +```text +instance Chain : Graph = chase { + ... +} +``` + +This marks an instance whose contents should be extended by the theory axioms. +Examples use this for transitive closure, existential witness generation, and +trace/reachability constructions. + +## Observed Design Patterns + +### Parameterized theories + +Theories can be abstract over: + +- a sort, such as `theory (X : Sort) Container` +- an instance, such as `theory (N : PetriNet instance) Marking` +- multiple arguments, such as `theory (N : PetriNet instance) (RP : N ReachabilityProblem instance) Solution` + +### Theory application by adjacency + +Theory arguments are written before the theory name. + +```text +N Marking instance +MyBase Map +ExampleNet problem0 Solution +``` + +### Nested structure via qualified names + +Many examples model dependent structure by naming into earlier declarations. + +```text +token/of : token -> N/P; +initial_iso : (trace/input_terminal) (RP/initial_marking/token) Iso instance; +``` + +## What Seems Outside the File DSL + +Some example comments refer to interactive commands such as: + +```text +:source +:load +:inspect +:chase +:solve +``` + +Those commands appear to belong to an external REPL or tool environment rather +than to the `.geolog` file grammar itself. + +## Best Example Files by Feature + +- `transitive_closure.geolog`: basic theory, axiom, and `= chase` usage +- `graph.geolog`: plain structural instances +- `monoid.geolog`: postfix application and positional record syntax +- `todo_list.geolog`: unary predicates and disjunction +- `sort_param_simple.geolog`: sort and instance parameters +- `nested_instance_test.geolog`: nested instance-valued fields +- `product_codomain_test.geolog`: record-valued function codomains +- `field_projection_test.geolog`: field projection syntax +- `record_existential_test.geolog`: existential witness creation with records +- `petri_net_showcase.geolog`: large multi-theory composition +- `solver_demo.geolog`: satisfiability-oriented axiom patterns + +## Minimal Example + +```text +theory Graph { + V : Sort; + Edge : [src: V, tgt: V] -> Prop; + Path : [src: V, tgt: V] -> Prop; + + ax/base : forall x, y : V. + [src: x, tgt: y] Edge |- [src: x, tgt: y] Path; +} + +instance Chain : Graph = chase { + a : V; + b : V; + [src: a, tgt: b] Edge; +} +``` + +That small example already shows the core structure of the DSL: + +- a `theory` +- sort and predicate declarations +- an axiom written as a sequent +- an `instance` +- a `chase` block that asks for closure under the theory axioms diff --git a/examples/geolog/category.geolog b/examples/geolog/category.geolog new file mode 100644 index 0000000..f480a1f --- /dev/null +++ b/examples/geolog/category.geolog @@ -0,0 +1,86 @@ +// Category theory in current geolog syntax +// +// This is the "desugared" version of the aspirational syntax in +// loose_thoughts/2026-01-21_dependent_sorts_and_functional_relations.md + +theory Category { + ob : Sort; + mor : Sort; + + // Morphism source and target + src : mor -> ob; + tgt : mor -> ob; + + // Composition: comp(f, g, h) means "h = f ; g" (f then g) + // Domain constraint: f.tgt = g.src + comp : [f: mor, g: mor, h: mor] -> Prop; + + // Identity: id(a, f) means "f is the identity on a" + id : [a: ob, f: mor] -> Prop; + + // === Axioms === + + // Identity morphisms have matching source and target + ax/id_src : forall x : ob, i : mor. [a: x, f: i] id |- i src = x; + ax/id_tgt : forall x : ob, i : mor. [a: x, f: i] id |- i tgt = x; + + // Composition domain constraint + ax/comp_dom : forall p : mor, q : mor, r : mor. + [f: p, g: q, h: r] comp |- p tgt = q src; + + // Composition source/target + ax/comp_src : forall p : mor, q : mor, r : mor. + [f: p, g: q, h: r] comp |- r src = p src; + ax/comp_tgt : forall p : mor, q : mor, r : mor. + [f: p, g: q, h: r] comp |- r tgt = q tgt; + + // Existence of identities (one per object) + ax/id_exists : forall x : ob. |- exists i : mor. [a: x, f: i] id; + + // Existence of composites (when composable) + ax/comp_exists : forall p : mor, q : mor. + p tgt = q src |- exists r : mor. [f: p, g: q, h: r] comp; + + // Left unit: id_a ; f = f + ax/unit_left : forall x : ob, i : mor, p : mor, r : mor. + [a: x, f: i] id, p src = x, [f: i, g: p, h: r] comp |- r = p; + + // Right unit: f ; id_b = f + ax/unit_right : forall y : ob, i : mor, p : mor, r : mor. + [a: y, f: i] id, p tgt = y, [f: p, g: i, h: r] comp |- r = p; + + // Associativity: (f ; g) ; h = f ; (g ; h) + ax/assoc : forall p : mor, q : mor, r : mor, pq : mor, qr : mor, pqr1 : mor, pqr2 : mor. + [f: p, g: q, h: pq] comp, [f: pq, g: r, h: pqr1] comp, + [f: q, g: r, h: qr] comp, [f: p, g: qr, h: pqr2] comp + |- pqr1 = pqr2; + + // Uniqueness of composition (functional) + ax/comp_unique : forall p : mor, q : mor, r1 : mor, r2 : mor. + [f: p, g: q, h: r1] comp, [f: p, g: q, h: r2] comp |- r1 = r2; + + // Uniqueness of identity (one per object) + ax/id_unique : forall x : ob, i1 : mor, i2 : mor. + [a: x, f: i1] id, [a: x, f: i2] id |- i1 = i2; +} + +// The "walking arrow" category: A --f--> B +// +// Now we can declare just objects and non-identity morphisms! +// The chase derives: +// - Identity morphisms for each object (via ax/id_exists) +// - Composition facts (via ax/comp_exists) +// - Source/target for compositions (via ax/comp_src, ax/comp_tgt) +// +// The equality saturation (via congruence closure) collapses: +// - id;id;id;... = id (via ax/unit_left and ax/unit_right) +// - Duplicate compositions (via ax/comp_unique) +// Without CC, the chase would loop forever creating id;id, id;id;id, ... +instance Arrow : Category = chase { + // Objects + A : ob; + B : ob; + + // Non-identity morphism + f : mor; f src = A; f tgt = B; +} diff --git a/examples/geolog/field_projection_chase_test.geolog b/examples/geolog/field_projection_chase_test.geolog new file mode 100644 index 0000000..a007482 --- /dev/null +++ b/examples/geolog/field_projection_chase_test.geolog @@ -0,0 +1,27 @@ +// Test: Field projection in chase + +theory FieldProjectionChaseTest { + A : Sort; + B : Sort; + + R : Sort; + R/data : R -> [x: A, y: B]; + + // Marker sort for elements whose x field matches a given a + XMatches : Sort; + XMatches/r : XMatches -> R; + XMatches/a : XMatches -> A; + + // Axiom: if r's x field equals a, create an XMatches + ax1 : forall r : R, a : A, b : B. r R/data = [x: a, y: b] |- exists m : XMatches. m XMatches/r = r, m XMatches/a = a; +} + +instance Test : FieldProjectionChaseTest = chase { + a1 : A; + a2 : A; + b1 : B; + r1 : R; + r1 R/data = [x: a1, y: b1]; + r2 : R; + r2 R/data = [x: a2, y: b1]; +} diff --git a/examples/geolog/field_projection_test.geolog b/examples/geolog/field_projection_test.geolog new file mode 100644 index 0000000..deb7376 --- /dev/null +++ b/examples/geolog/field_projection_test.geolog @@ -0,0 +1,12 @@ +// Test: Field projection syntax + +theory FieldProjectionTest { + A : Sort; + B : Sort; + + R : Sort; + R/data : R -> [x: A, y: B]; + + // Axiom using field projection: r R/data .x + ax1 : forall r : R, a : A. r R/data .x = a |- true; +} diff --git a/examples/geolog/graph.geolog b/examples/geolog/graph.geolog new file mode 100644 index 0000000..69ba7f5 --- /dev/null +++ b/examples/geolog/graph.geolog @@ -0,0 +1,79 @@ +// Directed Graph: vertices and edges with source/target functions +// +// This is the canonical example of a "presheaf" - a functor from a small +// category (the "walking arrow" • → •) to Set. + +theory Graph { + V : Sort; // Vertices + E : Sort; // Edges + + src : E -> V; // Source of an edge + tgt : E -> V; // Target of an edge +} + +// A simple triangle graph: A → B → C → A +instance Triangle : Graph = { + // Vertices + A : V; + B : V; + C : V; + + // Edges + ab : E; + bc : E; + ca : E; + + // Edge endpoints + ab src = A; + ab tgt = B; + bc src = B; + bc tgt = C; + ca src = C; + ca tgt = A; +} + +// A self-loop: one vertex with an edge to itself +instance Loop : Graph = { + v : V; + e : E; + e src = v; + e tgt = v; +} + +// The "walking arrow": two vertices, one edge +instance Arrow : Graph = { + s : V; + t : V; + f : E; + f src = s; + f tgt = t; +} + +// A more complex graph: diamond shape with two paths from top to bottom +// +// top +// / \ +// left right +// \ / +// bottom +// +instance Diamond : Graph = { + top : V; + left : V; + right : V; + bottom : V; + + top_left : E; + top_right : E; + left_bottom : E; + right_bottom : E; + + top_left src = top; + top_left tgt = left; + top_right src = top; + top_right tgt = right; + left_bottom src = left; + left_bottom tgt = bottom; + right_bottom src = right; + right_bottom tgt = bottom; +} diff --git a/examples/geolog/iso_instance_test.geolog b/examples/geolog/iso_instance_test.geolog new file mode 100644 index 0000000..68653c8 --- /dev/null +++ b/examples/geolog/iso_instance_test.geolog @@ -0,0 +1,29 @@ +// Multi-parameter theory instantiation test + +theory (X : Sort) (Y : Sort) Iso { + fwd : X -> Y; + bwd : Y -> X; + fb : forall x : X. |- x fwd bwd = x; + bf : forall y : Y. |- y bwd fwd = y; +} + +theory A { a : Sort; } +theory B { b : Sort; } + +instance As : A = { + a1 : a; + a2 : a; +} + +instance Bs : B = { + b1 : b; + b2 : b; +} + +// Can we create an Iso instance with sort parameters? +instance AB_Iso : As/a Bs/b Iso = { + a1 fwd = Bs/b1; + a2 fwd = Bs/b2; + b1 bwd = As/a1; + b2 bwd = As/a2; +} diff --git a/examples/geolog/iso_theory_test.geolog b/examples/geolog/iso_theory_test.geolog new file mode 100644 index 0000000..d17ad21 --- /dev/null +++ b/examples/geolog/iso_theory_test.geolog @@ -0,0 +1,9 @@ +// Multi-parameter theory test (Iso from vision) + +// First just try sorts as parameters +theory (X : Sort) (Y : Sort) Iso { + fwd : X -> Y; + bwd : Y -> X; + // Axioms would need chained function application... + // fb : forall x : X. |- x fwd bwd = x; +} diff --git a/examples/geolog/monoid.geolog b/examples/geolog/monoid.geolog new file mode 100644 index 0000000..596dd37 --- /dev/null +++ b/examples/geolog/monoid.geolog @@ -0,0 +1,78 @@ +// Monoid: a set with an associative binary operation and identity element +// +// This is the simplest algebraic structure with interesting axioms. +// Note: geolog uses postfix function application. + +theory Monoid { + M : Sort; + + // Binary operation: M × M → M + mul : [x: M, y: M] -> M; + + // Identity element: we use a unary function from M to M that + // "picks out" the identity (any x maps to e) + // A cleaner approach would use Unit → M but that needs product support. + id : M -> M; + + // Left identity: id(x) * y = y (id(x) is always e) + ax/left_id : forall x : M, y : M. + |- [x: x id, y: y] mul = y; + + // Right identity: x * id(y) = x + ax/right_id : forall x : M, y : M. + |- [x: x, y: y id] mul = x; + + // Associativity: (x * y) * z = x * (y * z) + ax/assoc : forall x : M, y : M, z : M. + |- [x: [x: x, y: y] mul, y: z] mul = [x: x, y: [x: y, y: z] mul] mul; + + // id is constant: id(x) = id(y) for all x, y + ax/id_const : forall x : M, y : M. + |- x id = y id; +} + +// Trivial monoid: single element, e * e = e +instance Trivial : Monoid = { + e : M; + + // Multiplication table: e * e = e + // Using positional syntax: [a, b] maps to [x: a, y: b] + [e, e] mul = e; + + // Identity: e is the identity element + e id = e; +} + +// Boolean "And" monoid: {T, F} with T as identity +// T and T = T, T and F = F, F and T = F, F and F = F +instance BoolAnd : Monoid = { + T : M; + F : M; + + // Identity: T is the identity element + T id = T; + F id = T; + + // Multiplication table for "and": + [x: T, y: T] mul = T; + [x: T, y: F] mul = F; + [x: F, y: T] mul = F; + [x: F, y: F] mul = F; +} + +// Boolean "Or" monoid: {T, F} with F as identity +// T or T = T, T or F = T, F or T = T, F or F = F +instance BoolOr : Monoid = { + T : M; + F : M; + + // Identity: F is the identity element + T id = F; + F id = F; + + // Multiplication table for "or": + [x: T, y: T] mul = T; + [x: T, y: F] mul = T; + [x: F, y: T] mul = T; + [x: F, y: F] mul = F; +} diff --git a/examples/geolog/nested_instance_test.geolog b/examples/geolog/nested_instance_test.geolog new file mode 100644 index 0000000..2182887 --- /dev/null +++ b/examples/geolog/nested_instance_test.geolog @@ -0,0 +1,33 @@ +// Test: Nested instance declarations (following vision pattern) + +theory Place { + P : Sort; +} + +theory (Pl : Place instance) Token { + token : Sort; + token/of : token -> Pl/P; +} + +theory (Pl : Place instance) Problem { + initial_marking : Pl Token instance; + target_marking : Pl Token instance; +} + +// Create a place instance +instance MyPlaces : Place = { + p1 : P; + p2 : P; +} + +// Test nested instance declarations +instance TestProblem : MyPlaces Problem = { + initial_marking = { + t1 : token; + t1 token/of = MyPlaces/p1; + }; + target_marking = { + t2 : token; + t2 token/of = MyPlaces/p2; + }; +} diff --git a/examples/geolog/petri_net.geolog b/examples/geolog/petri_net.geolog new file mode 100644 index 0000000..8e4e235 --- /dev/null +++ b/examples/geolog/petri_net.geolog @@ -0,0 +1,135 @@ +// Petri Net: a bipartite graph between places and transitions +// +// Petri nets model concurrent systems. Places hold tokens, transitions +// fire when their input places have tokens, consuming inputs and +// producing outputs. +// +// This encoding uses explicit "arc" sorts for input/output connections, +// which is more faithful to the categorical semantics (a span). + +theory PetriNet { + P : Sort; // Places + T : Sort; // Transitions + In : Sort; // Input arcs (from place to transition) + Out : Sort; // Output arcs (from transition to place) + + // Input arc endpoints + in/place : In -> P; + in/trans : In -> T; + + // Output arc endpoints + out/trans : Out -> T; + out/place : Out -> P; +} + +// A simple producer-consumer net: +// +// (ready) --[produce]--> (buffer) --[consume]--> (done) +// +instance ProducerConsumer : PetriNet = { + // Places + ready : P; + buffer : P; + done : P; + + // Transitions + produce : T; + consume : T; + + // Input arcs + i1 : In; + i1 in/place = ready; + i1 in/trans = produce; + + i2 : In; + i2 in/place = buffer; + i2 in/trans = consume; + + // Output arcs + o1 : Out; + o1 out/trans = produce; + o1 out/place = buffer; + + o2 : Out; + o2 out/trans = consume; + o2 out/place = done; +} + +// Mutual exclusion: two processes competing for a shared resource +// +// (idle1) --[enter1]--> (crit1) --[exit1]--> (idle1) +// ^ | +// | (mutex) | +// | v +// (idle2) --[enter2]--> (crit2) --[exit2]--> (idle2) +// +instance MutualExclusion : PetriNet = { + // Places for process 1 + idle1 : P; + crit1 : P; + + // Places for process 2 + idle2 : P; + crit2 : P; + + // Shared mutex token + mutex : P; + + // Transitions + enter1 : T; + exit1 : T; + enter2 : T; + exit2 : T; + + // Process 1 enters: needs idle1 AND mutex + i_enter1_idle : In; + i_enter1_idle in/place = idle1; + i_enter1_idle in/trans = enter1; + + i_enter1_mutex : In; + i_enter1_mutex in/place = mutex; + i_enter1_mutex in/trans = enter1; + + o_enter1 : Out; + o_enter1 out/trans = enter1; + o_enter1 out/place = crit1; + + // Process 1 exits: releases mutex + i_exit1 : In; + i_exit1 in/place = crit1; + i_exit1 in/trans = exit1; + + o_exit1_idle : Out; + o_exit1_idle out/trans = exit1; + o_exit1_idle out/place = idle1; + + o_exit1_mutex : Out; + o_exit1_mutex out/trans = exit1; + o_exit1_mutex out/place = mutex; + + // Process 2 enters: needs idle2 AND mutex + i_enter2_idle : In; + i_enter2_idle in/place = idle2; + i_enter2_idle in/trans = enter2; + + i_enter2_mutex : In; + i_enter2_mutex in/place = mutex; + i_enter2_mutex in/trans = enter2; + + o_enter2 : Out; + o_enter2 out/trans = enter2; + o_enter2 out/place = crit2; + + // Process 2 exits: releases mutex + i_exit2 : In; + i_exit2 in/place = crit2; + i_exit2 in/trans = exit2; + + o_exit2_idle : Out; + o_exit2_idle out/trans = exit2; + o_exit2_idle out/place = idle2; + + o_exit2_mutex : Out; + o_exit2_mutex out/trans = exit2; + o_exit2_mutex out/place = mutex; +} diff --git a/examples/geolog/petri_net_full.geolog b/examples/geolog/petri_net_full.geolog new file mode 100644 index 0000000..d4e3fe7 --- /dev/null +++ b/examples/geolog/petri_net_full.geolog @@ -0,0 +1,195 @@ +// Full Petri Net Reachability - Type-Theoretic Encoding +// +// This demonstrates the complete type-theoretic encoding of Petri net +// reachability from the original geolog design vision. +// +// Original design: loose_thoughts/2025-12-12_12:10_VanillaPetriNetRechability.md +// +// Key concepts: +// - PetriNet: places, transitions, input/output arcs (with proper arc semantics) +// - Marking: tokens in a net (parameterized by net) +// - ReachabilityProblem: initial and target markings (nested instances) +// - Trace: sequence of firings with wires connecting arcs +// - Iso: isomorphism between two sorts (used for bijections) +// - Solution: a trace with isomorphisms to markings +// +// This encoding is more type-theoretically precise than the simple +// PlaceReachability: it tracks individual tokens and arc multiplicities, +// enabling correct handling of "multi-token" transitions. + +// ============================================================ +// THEORY: PetriNet +// Basic structure: places, transitions, and arcs +// ============================================================ + +theory PetriNet { + P : Sort; // Places + T : Sort; // Transitions + + in : Sort; // Input arcs (place -> transition) + out : Sort; // Output arcs (transition -> place) + + // Each arc knows which place/transition it connects + in/src : in -> P; // Input arc source place + in/tgt : in -> T; // Input arc target transition + out/src : out -> T; // Output arc source transition + out/tgt : out -> P; // Output arc target place +} + +// ============================================================ +// THEORY: Marking (parameterized by N : PetriNet) +// A marking assigns tokens to places +// ============================================================ + +theory (N : PetriNet instance) Marking { + token : Sort; + token/of : token -> N/P; +} + +// ============================================================ +// THEORY: ReachabilityProblem (parameterized by N : PetriNet) +// Defines initial and target markings as nested instances +// ============================================================ + +theory (N : PetriNet instance) ReachabilityProblem { + initial_marking : N Marking instance; + target_marking : N Marking instance; +} + +// ============================================================ +// THEORY: Trace (parameterized by N : PetriNet) +// A trace is a sequence of transition firings with "wires" +// connecting input and output arcs +// ============================================================ + +theory (N : PetriNet instance) Trace { + // Firings + F : Sort; + F/of : F -> N/T; + + // Wires connect output of one firing to input of another + W : Sort; + W/src : W -> [firing : F, arc : N/out]; // Wire source (firing, output arc) + W/tgt : W -> [firing : F, arc : N/in]; // Wire target (firing, input arc) + + // Wire coherence: output arc must belong to source firing's transition + ax1 : forall w : W. |- w W/src .arc N/out/src = w W/src .firing F/of; + // Wire coherence: input arc must belong to target firing's transition + ax2 : forall w : W. |- w W/tgt .arc N/in/tgt = w W/tgt .firing F/of; + + // Wire uniqueness: each (firing, out-arc) pair has at most one wire + ax3 : forall w1, w2 : W. w1 W/src = w2 W/src |- w1 = w2; + // Wire uniqueness: each (firing, in-arc) pair has at most one wire + ax4 : forall w1, w2 : W. w1 W/tgt = w2 W/tgt |- w1 = w2; + + // Terminals: for initial marking tokens (input) and final marking tokens (output) + input_terminal : Sort; + output_terminal : Sort; + input_terminal/of : input_terminal -> N/P; + output_terminal/of : output_terminal -> N/P; + input_terminal/tgt : input_terminal -> [firing : F, arc : N/in]; + output_terminal/src : output_terminal -> [firing : F, arc : N/out]; + + // Every output arc of every firing must be wired OR be an output terminal + ax5 : forall f : F, arc : N/out. arc N/out/src = f F/of |- + (exists w : W. w W/src = [firing: f, arc: arc]) \/ + (exists o : output_terminal. o output_terminal/src = [firing: f, arc: arc]); + + // Every input arc of every firing must be wired OR be an input terminal + ax6 : forall f : F, arc : N/in. arc N/in/tgt = f F/of |- + (exists w : W. w W/tgt = [firing: f, arc: arc]) \/ + (exists i : input_terminal. i input_terminal/tgt = [firing: f, arc: arc]); +} + +// ============================================================ +// THEORY: Iso (parameterized by two sorts) +// An isomorphism between two sorts +// ============================================================ + +theory (X : Sort) (Y : Sort) Iso { + fwd : X -> Y; + bwd : Y -> X; + fb : forall x : X. |- x fwd bwd = x; + bf : forall y : Y. |- y bwd fwd = y; +} + +// ============================================================ +// THEORY: Solution (parameterized by N and RP) +// A solution to a reachability problem +// ============================================================ + +theory (N : PetriNet instance) (RP : N ReachabilityProblem instance) Solution { + // The witnessing trace + trace : N Trace instance; + + // Bijection between input terminals and initial marking tokens + initial_marking_iso : (trace/input_terminal) (RP/initial_marking/token) Iso instance; + + // Bijection between output terminals and target marking tokens + target_marking_iso : (trace/output_terminal) (RP/target_marking/token) Iso instance; + + // Initial marking commutes: token placement matches terminal placement + initial_marking_P_comm : forall i : trace/input_terminal. + |- i trace/input_terminal/of = i initial_marking_iso/fwd RP/initial_marking/token/of; + + // Target marking commutes: token placement matches terminal placement + target_marking_P_comm : forall o : trace/output_terminal. + |- o trace/output_terminal/of = o target_marking_iso/fwd RP/target_marking/token/of; +} + +// ============================================================ +// INSTANCE: ExampleNet - a small Petri net +// +// (A) --[ab]--> (B) --[bc]--> (C) +// ^ | +// +---[ba]------+ +// ============================================================ + +instance ExampleNet : PetriNet = { + // Places + A : P; + B : P; + C : P; + + // Transitions + ab : T; + ba : T; + bc : T; + + // A -> B (via ab) + ab_in : in; + ab_in in/src = A; + ab_in in/tgt = ab; + ab_out : out; + ab_out out/src = ab; + ab_out out/tgt = B; + + // B -> A (via ba) + ba_in : in; + ba_in in/src = B; + ba_in in/tgt = ba; + ba_out : out; + ba_out out/src = ba; + ba_out out/tgt = A; + + // B -> C (via bc) + bc_in : in; + bc_in in/src = B; + bc_in in/tgt = bc; + bc_out : out; + bc_out out/src = bc; + bc_out out/tgt = C; +} + +// ============================================================ +// Example queries (once query solving is implemented): +// +// query can_reach_B_from_A { +// ? : ExampleNet problem0 Solution instance; +// } +// +// where problem0 : ExampleNet ReachabilityProblem = { +// initial_marking = { tok : token; tok token/of = ExampleNet/A; }; +// target_marking = { tok : token; tok token/of = ExampleNet/B; }; +// } +// ============================================================ diff --git a/examples/geolog/petri_net_showcase.geolog b/examples/geolog/petri_net_showcase.geolog new file mode 100644 index 0000000..ece5de2 --- /dev/null +++ b/examples/geolog/petri_net_showcase.geolog @@ -0,0 +1,345 @@ +// Petri Net Reachability - Full Type-Theoretic Encoding +// +// This showcase demonstrates geolog's core capabilities through a +// non-trivial domain: encoding Petri net reachability as dependent types. +// +// A solution to a reachability problem is NOT a yes/no boolean but a +// CONSTRUCTIVE WITNESS: a diagrammatic proof that tokens can flow from +// initial to target markings via a sequence of transition firings. +// +// Key concepts demonstrated: +// - Parameterized theories (Marking depends on PetriNet instance) +// - Nested instance types (ReachabilityProblem contains Marking instances) +// - Sort-parameterized theories (Iso takes two sorts as parameters) +// - Cross-instance references (solution's trace elements reference problem's tokens) +// +// Original design: loose_thoughts/2025-12-12_12:10_VanillaPetriNetRechability.md + +// ============================================================ +// THEORY: PetriNet +// Places, transitions, and arcs with proper arc semantics +// ============================================================ + +theory PetriNet { + P : Sort; // Places + T : Sort; // Transitions + in : Sort; // Input arcs (place -> transition) + out : Sort; // Output arcs (transition -> place) + + in/src : in -> P; // Input arc source place + in/tgt : in -> T; // Input arc target transition + out/src : out -> T; // Output arc source transition + out/tgt : out -> P; // Output arc target place +} + +// ============================================================ +// THEORY: Marking (parameterized by N : PetriNet) +// A marking assigns tokens to places +// ============================================================ + +theory (N : PetriNet instance) Marking { + token : Sort; + token/of : token -> N/P; +} + +// ============================================================ +// THEORY: ReachabilityProblem (parameterized by N : PetriNet) +// Initial and target markings as nested instances +// ============================================================ + +theory (N : PetriNet instance) ReachabilityProblem { + initial_marking : N Marking instance; + target_marking : N Marking instance; +} + +// ============================================================ +// THEORY: Trace (parameterized by N : PetriNet) +// A trace records transition firings and token flow via wires +// ============================================================ +// +// A trace is a diagrammatic proof of reachability: +// - Firings represent transition occurrences +// - Wires connect output arcs of firings to input arcs of other firings +// - Terminals connect to the initial/target markings +// +// The completeness axiom (ax/must_be_fed) ensures every input arc +// of every firing is accounted for - either wired from another firing +// or fed by an input terminal. + +theory (N : PetriNet instance) Trace { + // Firings + F : Sort; + F/of : F -> N/T; + + // Wires connect output arcs of firings to input arcs of other firings + W : Sort; + W/src_firing : W -> F; + W/src_arc : W -> N/out; + W/tgt_firing : W -> F; + W/tgt_arc : W -> N/in; + + // Wire coherence: source arc must belong to source firing's transition + ax/wire_src_coherent : forall w : W. + |- w W/src_arc N/out/src = w W/src_firing F/of; + + // Wire coherence: target arc must belong to target firing's transition + ax/wire_tgt_coherent : forall w : W. + |- w W/tgt_arc N/in/tgt = w W/tgt_firing F/of; + + // Wire place coherence: wire connects matching places + ax/wire_place_coherent : forall w : W. + |- w W/src_arc N/out/tgt = w W/tgt_arc N/in/src; + + // Terminals + input_terminal : Sort; + output_terminal : Sort; + input_terminal/of : input_terminal -> N/P; + output_terminal/of : output_terminal -> N/P; + + // Terminals connect to specific firings and arcs + input_terminal/tgt_firing : input_terminal -> F; + input_terminal/tgt_arc : input_terminal -> N/in; + output_terminal/src_firing : output_terminal -> F; + output_terminal/src_arc : output_terminal -> N/out; + + // Terminal coherence axioms + ax/input_terminal_coherent : forall i : input_terminal. + |- i input_terminal/tgt_arc N/in/tgt = i input_terminal/tgt_firing F/of; + + ax/output_terminal_coherent : forall o : output_terminal. + |- o output_terminal/src_arc N/out/src = o output_terminal/src_firing F/of; + + // Terminal place coherence + ax/input_terminal_place : forall i : input_terminal. + |- i input_terminal/of = i input_terminal/tgt_arc N/in/src; + + ax/output_terminal_place : forall o : output_terminal. + |- o output_terminal/of = o output_terminal/src_arc N/out/tgt; + + // COMPLETENESS: Every arc of every firing must be accounted for. + + // Input completeness: every input arc must be fed by a wire or input terminal + ax/input_complete : forall f : F, arc : N/in. + arc N/in/tgt = f F/of |- + (exists w : W. w W/tgt_firing = f, w W/tgt_arc = arc) \/ + (exists i : input_terminal. i input_terminal/tgt_firing = f, i input_terminal/tgt_arc = arc); + + // Output completeness: every output arc must be captured by a wire or output terminal + ax/output_complete : forall f : F, arc : N/out. + arc N/out/src = f F/of |- + (exists w : W. w W/src_firing = f, w W/src_arc = arc) \/ + (exists o : output_terminal. o output_terminal/src_firing = f, o output_terminal/src_arc = arc); +} + +// ============================================================ +// THEORY: Iso (parameterized by two sorts) +// Isomorphism (bijection) between two sorts +// ============================================================ + +theory (X : Sort) (Y : Sort) Iso { + fwd : X -> Y; + bwd : Y -> X; + + // Roundtrip axioms ensure this is a true bijection + fb : forall x : X. |- x fwd bwd = x; + bf : forall y : Y. |- y bwd fwd = y; +} + +// ============================================================ +// THEORY: Solution (parameterized by N and RP) +// A constructive witness that target is reachable from initial +// ============================================================ + +theory (N : PetriNet instance) (RP : N ReachabilityProblem instance) Solution { + trace : N Trace instance; + + // Bijection: input terminals <-> initial marking tokens + initial_iso : (trace/input_terminal) (RP/initial_marking/token) Iso instance; + + // Bijection: output terminals <-> target marking tokens + target_iso : (trace/output_terminal) (RP/target_marking/token) Iso instance; + + // Commutativity axioms (currently unchecked): + // ax/init_comm : forall i : trace/input_terminal. + // |- i trace/input_terminal/of = i initial_iso/fwd RP/initial_marking/token/of; + // ax/target_comm : forall o : trace/output_terminal. + // |- o trace/output_terminal/of = o target_iso/fwd RP/target_marking/token/of; +} + +// ============================================================ +// INSTANCE: ExampleNet +// +// A Petri net with places A, B, C and transitions: +// ab: consumes 1 token from A, produces 1 token in B +// ba: consumes 1 token from B, produces 1 token in A +// abc: consumes 1 token from A AND 1 from B, produces 1 token in C +// +// +---[ba]----+ +// v | +// (A) --[ab]->(B) --+ +// | | +// +----[abc]-------+--> (C) +// +// The abc transition is interesting: it requires BOTH an A-token +// and a B-token to fire, producing a C-token. +// ============================================================ + +instance ExampleNet : PetriNet = { + A : P; B : P; C : P; + ab : T; ba : T; abc : T; + + // A -> B (via ab) + ab_in : in; ab_in in/src = A; ab_in in/tgt = ab; + ab_out : out; ab_out out/src = ab; ab_out out/tgt = B; + + // B -> A (via ba) + ba_in : in; ba_in in/src = B; ba_in in/tgt = ba; + ba_out : out; ba_out out/src = ba; ba_out out/tgt = A; + + // A + B -> C (via abc) - note: two input arcs! + abc_in1 : in; abc_in1 in/src = A; abc_in1 in/tgt = abc; + abc_in2 : in; abc_in2 in/src = B; abc_in2 in/tgt = abc; + abc_out : out; abc_out out/src = abc; abc_out out/tgt = C; +} + +// ============================================================ +// PROBLEM 0: Can we reach B from A with one token? +// Initial: 1 token in A +// Target: 1 token in B +// ============================================================ + +instance problem0 : ExampleNet ReachabilityProblem = { + initial_marking = { + tok : token; + tok token/of = ExampleNet/A; + }; + target_marking = { + tok : token; + tok token/of = ExampleNet/B; + }; +} + +// ============================================================ +// SOLUTION 0: Yes! Fire transition 'ab' once. +// +// This Solution instance is a CONSTRUCTIVE PROOF: +// - The trace contains one firing (f1) of transition 'ab' +// - The input terminal feeds the A-token into f1's input arc +// - The output terminal captures f1's B-token output +// - The isomorphisms prove the token counts match exactly +// ============================================================ + +instance solution0 : ExampleNet problem0 Solution = { + trace = { + // One firing of transition 'ab' + f1 : F; + f1 F/of = ExampleNet/ab; + + // Input terminal: feeds the initial A-token into f1 + it : input_terminal; + it input_terminal/of = ExampleNet/A; + it input_terminal/tgt_firing = f1; + it input_terminal/tgt_arc = ExampleNet/ab_in; + + // Output terminal: captures f1's B-token output + ot : output_terminal; + ot output_terminal/of = ExampleNet/B; + ot output_terminal/src_firing = f1; + ot output_terminal/src_arc = ExampleNet/ab_out; + }; + + initial_iso = { + trace/it fwd = problem0/initial_marking/tok; + problem0/initial_marking/tok bwd = trace/it; + }; + + target_iso = { + trace/ot fwd = problem0/target_marking/tok; + problem0/target_marking/tok bwd = trace/ot; + }; +} + +// ============================================================ +// PROBLEM 2: Can we reach C from two A-tokens? +// Initial: 2 tokens in A +// Target: 1 token in C +// +// This is interesting because the only path to C is via 'abc', +// which requires tokens in BOTH A and B simultaneously. +// ============================================================ + +instance problem2 : ExampleNet ReachabilityProblem = { + initial_marking = { + t1 : token; t1 token/of = ExampleNet/A; + t2 : token; t2 token/of = ExampleNet/A; + }; + target_marking = { + t : token; + t token/of = ExampleNet/C; + }; +} + +// ============================================================ +// SOLUTION 2: Yes! Fire 'ab' then 'abc'. +// +// Token flow diagram: +// +// [it1]--A-->[f1: ab]--B--wire-->[f2: abc]--C-->[ot] +// [it2]--A-----------------^ +// +// Step 1: Fire 'ab' to move one token A -> B +// - it1 feeds A-token into f1 via ab_in +// - f1 produces B-token via ab_out +// Step 2: Fire 'abc' consuming one A-token and one B-token +// - it2 feeds A-token into f2 via abc_in1 +// - Wire connects f1's ab_out to f2's abc_in2 (the B-input) +// - f2 produces C-token via abc_out +// ============================================================ + +instance solution2 : ExampleNet problem2 Solution = { + trace = { + // Two firings + f1 : F; f1 F/of = ExampleNet/ab; // First: A -> B + f2 : F; f2 F/of = ExampleNet/abc; // Second: A + B -> C + + // Wire connecting f1's B-output to f2's B-input + // This is the crucial connection that makes the trace valid! + w1 : W; + w1 W/src_firing = f1; + w1 W/src_arc = ExampleNet/ab_out; + w1 W/tgt_firing = f2; + w1 W/tgt_arc = ExampleNet/abc_in2; + + // Input terminal 1: feeds first A-token into f1 + it1 : input_terminal; + it1 input_terminal/of = ExampleNet/A; + it1 input_terminal/tgt_firing = f1; + it1 input_terminal/tgt_arc = ExampleNet/ab_in; + + // Input terminal 2: feeds second A-token into f2 + it2 : input_terminal; + it2 input_terminal/of = ExampleNet/A; + it2 input_terminal/tgt_firing = f2; + it2 input_terminal/tgt_arc = ExampleNet/abc_in1; + + // Output terminal: captures f2's C-token output + ot : output_terminal; + ot output_terminal/of = ExampleNet/C; + ot output_terminal/src_firing = f2; + ot output_terminal/src_arc = ExampleNet/abc_out; + }; + + // Bijection: 2 input terminals <-> 2 initial tokens + initial_iso = { + trace/it1 fwd = problem2/initial_marking/t1; + trace/it2 fwd = problem2/initial_marking/t2; + problem2/initial_marking/t1 bwd = trace/it1; + problem2/initial_marking/t2 bwd = trace/it2; + }; + + // Bijection: 1 output terminal <-> 1 target token + target_iso = { + trace/ot fwd = problem2/target_marking/t; + problem2/target_marking/t bwd = trace/ot; + }; +} diff --git a/examples/geolog/petri_net_solution.geolog b/examples/geolog/petri_net_solution.geolog new file mode 100644 index 0000000..4f3048f --- /dev/null +++ b/examples/geolog/petri_net_solution.geolog @@ -0,0 +1,188 @@ +// Full Petri Net Reachability with Synthesized Solution +// +// This file contains the complete type-theoretic encoding of Petri net +// reachability, plus a manually synthesized solution proving that place B +// is reachable from place A in the example net. +// +// ============================================================ +// This instance was synthesized automatically by Claude Opus 4.5. +// As was this entire file, and this entire project, really. +// ============================================================ + +// ============================================================ +// THEORY: PetriNet - Basic structure with arc semantics +// ============================================================ + +theory PetriNet { + P : Sort; // Places + T : Sort; // Transitions + in : Sort; // Input arcs (place -> transition) + out : Sort; // Output arcs (transition -> place) + + in/src : in -> P; // Input arc source place + in/tgt : in -> T; // Input arc target transition + out/src : out -> T; // Output arc source transition + out/tgt : out -> P; // Output arc target place +} + +// ============================================================ +// THEORY: Marking - Tokens parameterized by a net +// ============================================================ + +theory (N : PetriNet instance) Marking { + token : Sort; + token/of : token -> N/P; // Which place each token is in +} + +// ============================================================ +// THEORY: ReachabilityProblem - Initial and target markings +// ============================================================ + +theory (N : PetriNet instance) ReachabilityProblem { + initial_marking : N Marking instance; + target_marking : N Marking instance; +} + +// ============================================================ +// THEORY: Trace - A sequence of transition firings with wires +// ============================================================ +// +// Simplified version for now - full version with product types commented out below. + +theory (N : PetriNet instance) Trace { + F : Sort; // Firings + F/of : F -> N/T; // Which transition each fires + + // Terminals for initial/final marking tokens + input_terminal : Sort; + output_terminal : Sort; + input_terminal/of : input_terminal -> N/P; + output_terminal/of : output_terminal -> N/P; +} + +// Full Trace theory with wires and product types (not yet fully supported): +// +// theory (N : PetriNet instance) Trace { +// F : Sort; // Firings +// F/of : F -> N/T; // Which transition each fires +// +// W : Sort; // Wires connecting firings +// W/src : W -> [firing : F, arc : N/out]; // Wire source +// W/tgt : W -> [firing : F, arc : N/in]; // Wire target +// +// // Wire coherence axioms +// ax1 : forall w : W. |- w W/src .arc N/out/src = w W/src .firing F/of; +// ax2 : forall w : W. |- w W/tgt .arc N/in/tgt = w W/tgt .firing F/of; +// +// // Wire uniqueness +// ax3 : forall w1, w2 : W. w1 W/src = w2 W/src |- w1 = w2; +// ax4 : forall w1, w2 : W. w1 W/tgt = w2 W/tgt |- w1 = w2; +// +// // Terminals for initial/final marking tokens +// input_terminal : Sort; +// output_terminal : Sort; +// input_terminal/of : input_terminal -> N/P; +// output_terminal/of : output_terminal -> N/P; +// input_terminal/tgt : input_terminal -> [firing : F, arc : N/in]; +// output_terminal/src : output_terminal -> [firing : F, arc : N/out]; +// +// // Coverage axioms +// ax5 : forall f : F, arc : N/out. arc N/out/src = f F/of |- +// (exists w : W. w W/src = [firing: f, arc: arc]) \/ +// (exists o : output_terminal. o output_terminal/src = [firing: f, arc: arc]); +// ax6 : forall f : F, arc : N/in. arc N/in/tgt = f F/of |- +// (exists w : W. w W/tgt = [firing: f, arc: arc]) \/ +// (exists i : input_terminal. i input_terminal/tgt = [firing: f, arc: arc]); +// } + +// ============================================================ +// THEORY: Iso - Isomorphism between two sorts +// ============================================================ + +theory (X : Sort) (Y : Sort) Iso { + fwd : X -> Y; + bwd : Y -> X; + fb : forall x : X. |- x fwd bwd = x; + bf : forall y : Y. |- y bwd fwd = y; +} + +// ============================================================ +// THEORY: Solution - A complete reachability witness +// ============================================================ + +theory (N : PetriNet instance) (RP : N ReachabilityProblem instance) Solution { + trace : N Trace instance; + + initial_iso : (trace/input_terminal) (RP/initial_marking/token) Iso instance; + target_iso : (trace/output_terminal) (RP/target_marking/token) Iso instance; + + ax/init_comm : forall i : trace/input_terminal. + |- i trace/input_terminal/of = i initial_iso/fwd RP/initial_marking/token/of; + ax/target_comm : forall o : trace/output_terminal. + |- o trace/output_terminal/of = o target_iso/fwd RP/target_marking/token/of; +} + +// ============================================================ +// INSTANCE: ExampleNet - A small Petri net +// +// (A) --[ab]--> (B) --[bc]--> (C) +// ^ | +// +---[ba]------+ +// ============================================================ + +instance ExampleNet : PetriNet = { + A : P; B : P; C : P; + ab : T; ba : T; bc : T; + + ab_in : in; ab_in in/src = A; ab_in in/tgt = ab; + ab_out : out; ab_out out/src = ab; ab_out out/tgt = B; + + ba_in : in; ba_in in/src = B; ba_in in/tgt = ba; + ba_out : out; ba_out out/src = ba; ba_out out/tgt = A; + + bc_in : in; bc_in in/src = B; bc_in in/tgt = bc; + bc_out : out; bc_out out/src = bc; bc_out out/tgt = C; +} + +// ============================================================ +// INSTANCE: problem0 - Can we reach B from A? +// ============================================================ + +instance problem0 : ExampleNet ReachabilityProblem = { + initial_marking = { + tok : token; + tok token/of = ExampleNet/A; + }; + target_marking = { + tok : token; + tok token/of = ExampleNet/B; + }; +} + +// ============================================================ +// INSTANCE: solution0 - YES! Here's the proof. +// ============================================================ +// This instance was synthesized automatically by Claude Opus 4.5. +// ============================================================ + +// The solution proves that place B is reachable from place A by firing +// transition ab. This creates a trace with one firing and the necessary +// input/output terminal mappings. + +instance solution0 : ExampleNet problem0 Solution = { + trace = { + f1 : F; + f1 F/of = ExampleNet/ab; + + it : input_terminal; + it input_terminal/of = ExampleNet/A; + + ot : output_terminal; + ot output_terminal/of = ExampleNet/B; + }; + + // NOTE: Cross-instance references (e.g., trace/it in initial_iso) + // are not yet fully supported. The iso instances would map: + // - trace/it <-> problem0/initial_marking/tok + // - trace/ot <-> problem0/target_marking/tok +} diff --git a/examples/geolog/petri_reachability.geolog b/examples/geolog/petri_reachability.geolog new file mode 100644 index 0000000..fb5a453 --- /dev/null +++ b/examples/geolog/petri_reachability.geolog @@ -0,0 +1,164 @@ +// Petri Net Reachability - Full Example +// +// This demonstrates the core ideas from the original geolog design document: +// modeling Petri net reachability using geometric logic with the chase algorithm. +// +// Original design: loose_thoughts/2025-12-12_12:10.md +// +// Key concepts: +// - PetriNet: places, transitions, input/output arcs +// - Marking: assignment of tokens to places (parameterized theory) +// - Trace: sequence of transition firings connecting markings +// - Reachability: computed via chase algorithm + +// ============================================================ +// THEORY: PetriNet +// ============================================================ + +theory PetriNet { + P : Sort; // Places + T : Sort; // Transitions + In : Sort; // Input arcs (place -> transition) + Out : Sort; // Output arcs (transition -> place) + + // Arc structure + in/place : In -> P; + in/trans : In -> T; + out/trans : Out -> T; + out/place : Out -> P; +} + +// ============================================================ +// THEORY: Marking (parameterized) +// A marking assigns tokens to places in a specific net +// ============================================================ + +theory (N : PetriNet instance) Marking { + Token : Sort; + of : Token -> N/P; +} + +// ============================================================ +// THEORY: PlaceReachability +// Simplified reachability at the place level +// ============================================================ + +theory PlaceReachability { + P : Sort; + T : Sort; + + // Which transition connects which places + // Fires(t, from, to) means transition t can move a token from 'from' to 'to' + Fires : [trans: T, from: P, to: P] -> Prop; + + // Reachability relation (transitive closure) + CanReach : [from: P, to: P] -> Prop; + + // Reflexivity: every place can reach itself + ax/refl : forall p : P. + |- [from: p, to: p] CanReach; + + // Transition firing creates reachability + ax/fire : forall t : T, x : P, y : P. + [trans: t, from: x, to: y] Fires |- [from: x, to: y] CanReach; + + // Transitivity: reachability composes + ax/trans : forall x : P, y : P, z : P. + [from: x, to: y] CanReach, [from: y, to: z] CanReach |- [from: x, to: z] CanReach; +} + +// ============================================================ +// INSTANCE: SimpleNet +// A -> B -> C with bidirectional A <-> B +// +// (A) <--[ba]-- (B) --[bc]--> (C) +// | ^ +// +---[ab]------+ +// ============================================================ + +// Uses chase to derive CanReach from axioms (reflexivity, fire, transitivity) +instance SimpleNet : PlaceReachability = chase { + // Places + A : P; + B : P; + C : P; + + // Transitions + ab : T; // A -> B + ba : T; // B -> A + bc : T; // B -> C + + // Firing relations + [trans: ab, from: A, to: B] Fires; + [trans: ba, from: B, to: A] Fires; + [trans: bc, from: B, to: C] Fires; +} + +// ============================================================ +// INSTANCE: MutexNet +// Two processes competing for a mutex +// +// idle1 --[enter1]--> crit1 --[exit1]--> idle1 +// ^ | +// | mutex | +// | v +// idle2 --[enter2]--> crit2 --[exit2]--> idle2 +// ============================================================ + +// Uses chase to derive reachability relation +instance MutexNet : PlaceReachability = chase { + // Places + idle1 : P; + crit1 : P; + idle2 : P; + crit2 : P; + mutex : P; + + // Transitions + enter1 : T; + exit1 : T; + enter2 : T; + exit2 : T; + + // Process 1 acquires mutex: idle1 + mutex -> crit1 + // (simplified: we track place-level, not token-level) + [trans: enter1, from: idle1, to: crit1] Fires; + [trans: enter1, from: mutex, to: crit1] Fires; + + // Process 1 releases mutex: crit1 -> idle1 + mutex + [trans: exit1, from: crit1, to: idle1] Fires; + [trans: exit1, from: crit1, to: mutex] Fires; + + // Process 2 acquires mutex: idle2 + mutex -> crit2 + [trans: enter2, from: idle2, to: crit2] Fires; + [trans: enter2, from: mutex, to: crit2] Fires; + + // Process 2 releases mutex: crit2 -> idle2 + mutex + [trans: exit2, from: crit2, to: idle2] Fires; + [trans: exit2, from: crit2, to: mutex] Fires; +} + +// ============================================================ +// INSTANCE: ProducerConsumerNet +// Producer creates items, consumer processes them +// +// ready --[produce]--> buffer --[consume]--> done +// ============================================================ + +// Uses chase to derive reachability relation +instance ProducerConsumerNet : PlaceReachability = chase { + // Places + ready : P; + buffer : P; + done : P; + + // Transitions + produce : T; + consume : T; + + // Produce: ready -> buffer + [trans: produce, from: ready, to: buffer] Fires; + + // Consume: buffer -> done + [trans: consume, from: buffer, to: done] Fires; +} diff --git a/examples/geolog/petri_reachability_full_vision.geolog b/examples/geolog/petri_reachability_full_vision.geolog new file mode 100644 index 0000000..a3155f5 --- /dev/null +++ b/examples/geolog/petri_reachability_full_vision.geolog @@ -0,0 +1,72 @@ +// Full Petri Net Reachability Vision Test +// From 2025-12-12_12:10_VanillaPetriNetRechability.md + +theory PetriNet { + P : Sort; + T : Sort; + in : Sort; + out : Sort; + in/src : in -> P; + in/tgt : in -> T; + out/src : out -> T; + out/tgt : out -> P; +} + +theory (N : PetriNet instance) Marking { + token : Sort; + token/of : token -> N/P; +} + +theory (N : PetriNet instance) ReachabilityProblem { + initial_marking : N Marking instance; + target_marking : N Marking instance; +} + +// Simplified Trace theory without disjunctions for now +theory (N : PetriNet instance) SimpleTrace { + F : Sort; + F/of : F -> N/T; + + input_terminal : Sort; + output_terminal : Sort; + input_terminal/of : input_terminal -> N/P; + output_terminal/of : output_terminal -> N/P; + input_terminal/tgt : input_terminal -> [firing : F, arc : N/in]; + output_terminal/src : output_terminal -> [firing : F, arc : N/out]; + + // Simplified ax5: every firing+arc gets an output terminal + ax5 : forall f : F, arc : N/out. |- exists o : output_terminal. o output_terminal/src = [firing: f, arc: arc]; + + // Simplified ax6: every firing+arc gets an input terminal + ax6 : forall f : F, arc : N/in. |- exists i : input_terminal. i input_terminal/tgt = [firing: f, arc: arc]; +} + +instance ExampleNet : PetriNet = { + A : P; + B : P; + ab : T; + ab_in : in; + ab_in in/src = A; + ab_in in/tgt = ab; + ab_out : out; + ab_out out/src = ab; + ab_out out/tgt = B; +} + +// Test nested instance elaboration +instance problem0 : ExampleNet ReachabilityProblem = { + initial_marking = { + tok : token; + tok token/of = ExampleNet/A; + }; + target_marking = { + tok : token; + tok token/of = ExampleNet/B; + }; +} + +// Test chase with SimpleTrace +instance trace0 : ExampleNet SimpleTrace = chase { + f1 : F; + f1 F/of = ExampleNet/ab; +} diff --git a/examples/geolog/petri_reachability_vision.geolog b/examples/geolog/petri_reachability_vision.geolog new file mode 100644 index 0000000..20ef578 --- /dev/null +++ b/examples/geolog/petri_reachability_vision.geolog @@ -0,0 +1,94 @@ +// Petri Net Reachability Vision Test +// Based on 2025-12-12 design document + +// Basic Petri net structure +theory PetriNet { + // Places + P : Sort; + + // Transitions + T : Sort; + + // Arcs (input to transitions, output from transitions) + in : Sort; + out : Sort; + in/src : in -> P; + in/tgt : in -> T; + out/src : out -> T; + out/tgt : out -> P; +} + +// A marking is a multiset of tokens, each at a place +theory (N : PetriNet instance) Marking { + token : Sort; + token/of : token -> N/P; +} + +// A reachability problem is: can we get from initial marking to target? +theory (N : PetriNet instance) ReachabilityProblem { + initial_marking : N Marking instance; + target_marking : N Marking instance; +} + +// A trace is a sequence of firings connected by wires +theory (N : PetriNet instance) Trace { + // Firings of transitions + F : Sort; + F/of : F -> N/T; + + // Wires connect firing outputs to firing inputs + W : Sort; + W/src : W -> [firing : F, arc : N/out]; + W/tgt : W -> [firing : F, arc : N/in]; + + // Terminals are unconnected arc endpoints (to/from the initial/target markings) + input_terminal : Sort; + output_terminal : Sort; + input_terminal/of : input_terminal -> N/P; + output_terminal/of : output_terminal -> N/P; + input_terminal/tgt : input_terminal -> [firing : F, arc : N/in]; + output_terminal/src : output_terminal -> [firing : F, arc : N/out]; +} + +// Example Petri net: A <--ab/ba--> B, (A,B) --abc--> C +instance ExampleNet : PetriNet = { + A : P; + B : P; + C : P; + ab : T; + ba : T; + abc : T; + ab_in : in; + ab_in in/src = A; + ab_in in/tgt = ab; + ab_out : out; + ab_out out/src = ab; + ab_out out/tgt = B; + ba_in : in; + ba_in in/src = B; + ba_in in/tgt = ba; + ba_out : out; + ba_out out/src = ba; + ba_out out/tgt = A; + abc_in1 : in; + abc_in1 in/src = A; + abc_in1 in/tgt = abc; + abc_in2 : in; + abc_in2 in/src = B; + abc_in2 in/tgt = abc; + abc_out : out; + abc_out out/src = abc; + abc_out out/tgt = C; +} + +// Reachability problem: Can we reach B from A? +instance problem0 : ExampleNet ReachabilityProblem = { + initial_marking = { + t : token; + t token/of = ExampleNet/A; + }; + target_marking = { + t : token; + t token/of = ExampleNet/B; + }; +} diff --git a/examples/geolog/petri_trace_axioms.geolog b/examples/geolog/petri_trace_axioms.geolog new file mode 100644 index 0000000..1295e0c --- /dev/null +++ b/examples/geolog/petri_trace_axioms.geolog @@ -0,0 +1,66 @@ +// Test Trace theory with axioms using product codomains + +theory PetriNet { + P : Sort; + T : Sort; + in : Sort; + out : Sort; + in/src : in -> P; + in/tgt : in -> T; + out/src : out -> T; + out/tgt : out -> P; +} + +// Trace theory with axioms +theory (N : PetriNet instance) Trace { + F : Sort; + F/of : F -> N/T; + + W : Sort; + W/src : W -> [firing : F, arc : N/out]; + W/tgt : W -> [firing : F, arc : N/in]; + + input_terminal : Sort; + output_terminal : Sort; + input_terminal/of : input_terminal -> N/P; + output_terminal/of : output_terminal -> N/P; + input_terminal/tgt : input_terminal -> [firing : F, arc : N/in]; + output_terminal/src : output_terminal -> [firing : F, arc : N/out]; + + // Axiom: wires are injective on source + // forall w1, w2 : W. w1 W/src = w2 W/src |- w1 = w2; + // (Commented out - requires product codomain equality in premises) + + // Axiom: every arc endpoint must be wired or terminated + // forall f : F, arc : N/out. arc N/out/src = f F/of |- + // (exists w : W. w W/src = [firing: f, arc: arc]) \/ + // (exists o : output_terminal. o output_terminal/src = [firing: f, arc: arc]); + // (Commented out - requires product codomain values in conclusions) +} + +// Simple net for testing +instance SimpleNet : PetriNet = { + A : P; + B : P; + t : T; + arc_in : in; + arc_in in/src = A; + arc_in in/tgt = t; + arc_out : out; + arc_out out/src = t; + arc_out out/tgt = B; +} + +// Test that the basic theory without axioms still works +instance SimpleTrace : SimpleNet Trace = { + f1 : F; + f1 F/of = SimpleNet/t; + + it : input_terminal; + it input_terminal/of = SimpleNet/A; + it input_terminal/tgt = [firing: f1, arc: SimpleNet/arc_in]; + + ot : output_terminal; + ot output_terminal/of = SimpleNet/B; + ot output_terminal/src = [firing: f1, arc: SimpleNet/arc_out]; +} diff --git a/examples/geolog/petri_trace_coverage_test.geolog b/examples/geolog/petri_trace_coverage_test.geolog new file mode 100644 index 0000000..dd3c2f2 --- /dev/null +++ b/examples/geolog/petri_trace_coverage_test.geolog @@ -0,0 +1,36 @@ +// Test: Trace coverage axiom (simplified) + +theory PetriNet { + P : Sort; + T : Sort; + out : Sort; + out/src : out -> T; + out/tgt : out -> P; +} + +theory (N : PetriNet instance) Trace { + F : Sort; + F/of : F -> N/T; + + output_terminal : Sort; + output_terminal/src : output_terminal -> [firing : F, arc : N/out]; + + // Simplified ax5: for every arc and firing, if the arc's source is the firing's transition, + // create an output terminal + ax5 : forall f : F, arc : N/out. |- exists o : output_terminal. o output_terminal/src = [firing: f, arc: arc]; +} + +instance SimpleNet : PetriNet = { + A : P; + B : P; + t : T; + arc_out : out; + arc_out out/src = t; + arc_out out/tgt = B; +} + +// Trace with just a firing - chase should create a terminal +instance TestTrace : SimpleNet Trace = chase { + f1 : F; + f1 F/of = SimpleNet/t; +} diff --git a/examples/geolog/petri_trace_full_vision.geolog b/examples/geolog/petri_trace_full_vision.geolog new file mode 100644 index 0000000..687cac8 --- /dev/null +++ b/examples/geolog/petri_trace_full_vision.geolog @@ -0,0 +1,57 @@ +// Trace theory with wires and disjunctions +// Testing the full vision from 2025-12-12 + +theory PetriNet { + P : Sort; + T : Sort; + in : Sort; + out : Sort; + in/src : in -> P; + in/tgt : in -> T; + out/src : out -> T; + out/tgt : out -> P; +} + +theory (N : PetriNet instance) Trace { + F : Sort; + F/of : F -> N/T; + + W : Sort; + W/src : W -> [firing : F, arc : N/out]; + W/tgt : W -> [firing : F, arc : N/in]; + + input_terminal : Sort; + output_terminal : Sort; + input_terminal/of : input_terminal -> N/P; + output_terminal/of : output_terminal -> N/P; + input_terminal/tgt : input_terminal -> [firing : F, arc : N/in]; + output_terminal/src : output_terminal -> [firing : F, arc : N/out]; + + // Every out arc of every firing: either wired or terminal + ax5 : forall f : F, arc : N/out. |- + (exists w : W. w W/src = [firing: f, arc: arc]) \/ + (exists o : output_terminal. o output_terminal/src = [firing: f, arc: arc]); + + // Every in arc of every firing: either wired or terminal + ax6 : forall f : F, arc : N/in. |- + (exists w : W. w W/tgt = [firing: f, arc: arc]) \/ + (exists i : input_terminal. i input_terminal/tgt = [firing: f, arc: arc]); +} + +instance SimpleNet : PetriNet = { + A : P; + B : P; + t : T; + arc_in : in; + arc_in in/src = A; + arc_in in/tgt = t; + arc_out : out; + arc_out out/src = t; + arc_out out/tgt = B; +} + +// Chase should create both wires AND terminals (naive chase adds all disjuncts) +instance trace_test : SimpleNet Trace = chase { + f1 : F; + f1 F/of = SimpleNet/t; +} diff --git a/examples/geolog/petri_trace_test.geolog b/examples/geolog/petri_trace_test.geolog new file mode 100644 index 0000000..0a3a674 --- /dev/null +++ b/examples/geolog/petri_trace_test.geolog @@ -0,0 +1,58 @@ +// Test that Trace theory with product codomains works + +theory PetriNet { + P : Sort; + T : Sort; + in : Sort; + out : Sort; + in/src : in -> P; + in/tgt : in -> T; + out/src : out -> T; + out/tgt : out -> P; +} + +// Simple Petri net: A --t--> B +instance SimpleNet : PetriNet = { + A : P; + B : P; + t : T; + arc_in : in; + arc_in in/src = A; + arc_in in/tgt = t; + arc_out : out; + arc_out out/src = t; + arc_out out/tgt = B; +} + +// Trace theory with product codomains for wire endpoints +theory (N : PetriNet instance) Trace { + F : Sort; + F/of : F -> N/T; + + W : Sort; + W/src : W -> [firing : F, arc : N/out]; + W/tgt : W -> [firing : F, arc : N/in]; + + input_terminal : Sort; + output_terminal : Sort; + input_terminal/of : input_terminal -> N/P; + output_terminal/of : output_terminal -> N/P; + input_terminal/tgt : input_terminal -> [firing : F, arc : N/in]; + output_terminal/src : output_terminal -> [firing : F, arc : N/out]; +} + +// A simple trace: one firing of t, with input/output terminals +instance SimpleTrace : SimpleNet Trace = { + f1 : F; + f1 F/of = SimpleNet/t; + + // Input terminal (token comes from external marking) + it : input_terminal; + it input_terminal/of = SimpleNet/A; + it input_terminal/tgt = [firing: f1, arc: SimpleNet/arc_in]; + + // Output terminal (token goes to external marking) + ot : output_terminal; + ot output_terminal/of = SimpleNet/B; + ot output_terminal/src = [firing: f1, arc: SimpleNet/arc_out]; +} diff --git a/examples/geolog/preorder.geolog b/examples/geolog/preorder.geolog new file mode 100644 index 0000000..47983a0 --- /dev/null +++ b/examples/geolog/preorder.geolog @@ -0,0 +1,42 @@ +// Preorder: a set with a reflexive, transitive relation +// +// This demonstrates RELATIONS (predicates) as opposed to functions. +// A relation R : A -> Prop is a predicate on A. +// For binary relations, we use a product domain: R : [x: A, y: A] -> Prop + +theory Preorder { + X : Sort; + + // The ordering relation: x ≤ y + leq : [x: X, y: X] -> Prop; + + // Reflexivity: x ≤ x + ax/refl : forall x : X. + |- [x: x, y: x] leq; + + // Transitivity: x ≤ y ∧ y ≤ z → x ≤ z + ax/trans : forall x : X, y : X, z : X. + [x: x, y: y] leq, [x: y, y: z] leq |- [x: x, y: z] leq; +} + +// The discrete preorder: only reflexive pairs +// (no elements are comparable except to themselves) +// Uses `chase` to automatically derive reflexive pairs from axiom ax/refl. +instance Discrete3 : Preorder = chase { + a : X; + b : X; + c : X; +} + +// A total order on 3 elements: a ≤ b ≤ c +// Uses `chase` to derive reflexive and transitive closure. +instance Chain3 : Preorder = chase { + bot : X; + mid : X; + top : X; + + // Assert the basic ordering; chase will add reflexive pairs + // and transitive closure (bot ≤ top) + [x: bot, y: mid] leq; + [x: mid, y: top] leq; +} diff --git a/examples/geolog/product_codomain_equality_test.geolog b/examples/geolog/product_codomain_equality_test.geolog new file mode 100644 index 0000000..9a86219 --- /dev/null +++ b/examples/geolog/product_codomain_equality_test.geolog @@ -0,0 +1,23 @@ +// Test: Product codomain equality in premise (ax3 pattern) + +theory ProductCodomainEqTest { + A : Sort; + B : Sort; + + W : Sort; + W/src : W -> [x: A, y: B]; + + // ax3 pattern: forall w1, w2 : W. w1 W/src = w2 W/src |- w1 = w2 + // This should make W injective on src + ax_inj : forall w1 : W, w2 : W. w1 W/src = w2 W/src |- w1 = w2; +} + +// Instance with two wires that have the same src - should be identified by chase +instance Test : ProductCodomainEqTest = { + a1 : A; + b1 : B; + w1 : W; + w1 W/src = [x: a1, y: b1]; + w2 : W; + w2 W/src = [x: a1, y: b1]; +} diff --git a/examples/geolog/product_codomain_test.geolog b/examples/geolog/product_codomain_test.geolog new file mode 100644 index 0000000..b804354 --- /dev/null +++ b/examples/geolog/product_codomain_test.geolog @@ -0,0 +1,51 @@ +// Test: Product Codomain Support +// +// This tests the new feature where functions can have product codomains, +// allowing record literal assignments like: +// elem func = [field1: v1, field2: v2]; + +theory ProductCodomainTest { + A : Sort; + B : Sort; + C : Sort; + + // Function with product codomain: maps A elements to (B, C) pairs + pair_of : A -> [left: B, right: C]; +} + +instance TestInstance : ProductCodomainTest = { + // Elements + a1 : A; + b1 : B; + b2 : B; + c1 : C; + + // Assign product codomain value using record literal + a1 pair_of = [left: b1, right: c1]; +} + +// A more realistic example: Edges in a graph +theory DirectedGraph { + V : Sort; + E : Sort; + + // Edge endpoints as a product codomain + endpoints : E -> [src: V, tgt: V]; +} + +instance TriangleGraph : DirectedGraph = { + // Vertices + v0 : V; + v1 : V; + v2 : V; + + // Edges + e01 : E; + e12 : E; + e20 : E; + + // Assign edge endpoints using record literals + e01 endpoints = [src: v0, tgt: v1]; + e12 endpoints = [src: v1, tgt: v2]; + e20 endpoints = [src: v2, tgt: v0]; +} diff --git a/examples/geolog/record_existential_test.geolog b/examples/geolog/record_existential_test.geolog new file mode 100644 index 0000000..f1d2fbe --- /dev/null +++ b/examples/geolog/record_existential_test.geolog @@ -0,0 +1,18 @@ +// Test: Record literals in existential conclusions + +theory RecordExistentialTest { + A : Sort; + B : Sort; + + R : Sort; + R/data : R -> [x: A, y: B]; + + // Axiom: given any a:A and b:B, there exists an R with that data + ax1 : forall a : A, b : B. |- + exists r : R. r R/data = [x: a, y: b]; +} + +instance Test : RecordExistentialTest = chase { + a1 : A; + b1 : B; +} diff --git a/examples/geolog/record_in_axiom_test.geolog b/examples/geolog/record_in_axiom_test.geolog new file mode 100644 index 0000000..559139d --- /dev/null +++ b/examples/geolog/record_in_axiom_test.geolog @@ -0,0 +1,12 @@ +// Test: Record literals in axioms + +theory RecordAxiomTest { + A : Sort; + B : Sort; + + R : Sort; + R/data : R -> [x: A, y: B]; + + // Test axiom with record literal RHS + ax1 : forall r : R, a : A, b : B. r R/data = [x: a, y: b] |- true; +} diff --git a/examples/geolog/record_premise_chase_test.geolog b/examples/geolog/record_premise_chase_test.geolog new file mode 100644 index 0000000..5f67156 --- /dev/null +++ b/examples/geolog/record_premise_chase_test.geolog @@ -0,0 +1,23 @@ +// Test: Chase with record literals in premises + +theory RecordPremiseTest { + A : Sort; + B : Sort; + + R : Sort; + R/data : R -> [x: A, y: B]; + + // Derived sort for processed items + Processed : Sort; + Processed/r : Processed -> R; + + // Axiom: given r with data [x: a, y: b], create a Processed for it + ax1 : forall r : R, a : A, b : B. r R/data = [x: a, y: b] |- exists p : Processed. p Processed/r = r; +} + +instance Test : RecordPremiseTest = { + a1 : A; + b1 : B; + r1 : R; + r1 R/data = [x: a1, y: b1]; +} diff --git a/examples/geolog/relalg_simple.geolog b/examples/geolog/relalg_simple.geolog new file mode 100644 index 0000000..39aebff --- /dev/null +++ b/examples/geolog/relalg_simple.geolog @@ -0,0 +1,130 @@ +// Example: RelAlgIR query plan instances +// +// This demonstrates creating query plans as RelAlgIR instances. +// These show the string diagram representation of relational algebra. +// +// First we need to load both GeologMeta (for Srt, Func, etc.) and RelAlgIR. +// This file just defines instances; load theories first in the REPL: +// :load theories/GeologMeta.geolog +// :load theories/RelAlgIR.geolog +// :load examples/geolog/relalg_simple.geolog +// +// Note: RelAlgIR extends GeologMeta, so a RelAlgIR instance contains +// elements from both GeologMeta sorts (Srt, Func, Elem) and RelAlgIR +// sorts (Wire, Schema, ScanOp, etc.) + +// ============================================================ +// Example 1: Simple Scan +// ============================================================ +// Query: "scan all elements of sort V" +// Plan: () --[ScanOp]--> Wire + +instance ScanV : RelAlgIR = chase { + // -- Schema (target theory) -- + target_theory : GeologMeta/Theory; + target_theory GeologMeta/Theory/parent = target_theory; + + v_srt : GeologMeta/Srt; + v_srt GeologMeta/Srt/theory = target_theory; + + // -- Query Plan -- + v_base_schema : BaseSchema; + v_base_schema BaseSchema/srt = v_srt; + + v_schema : Schema; + v_base_schema BaseSchema/schema = v_schema; + + scan_out : Wire; + scan_out Wire/schema = v_schema; + + scan : ScanOp; + scan ScanOp/srt = v_srt; + scan ScanOp/out = scan_out; + + scan_op : Op; + scan ScanOp/op = scan_op; +} + +// ============================================================ +// Example 2: Filter(Scan) +// ============================================================ +// Query: "scan E, filter where src(e) = some vertex" +// Plan: () --[Scan]--> w1 --[Filter]--> w2 +// +// This demonstrates composition via wire sharing. + +// Uses chase to derive relations. +instance FilterScan : RelAlgIR = chase { + // -- Schema (representing Graph theory) -- + target_theory : GeologMeta/Theory; + target_theory GeologMeta/Theory/parent = target_theory; + + // Sorts: V (vertices), E (edges) + v_srt : GeologMeta/Srt; + v_srt GeologMeta/Srt/theory = target_theory; + + e_srt : GeologMeta/Srt; + e_srt GeologMeta/Srt/theory = target_theory; + + // Functions: src : E -> V + // First create the DSort wrappers + v_base_ds : GeologMeta/BaseDS; + v_base_ds GeologMeta/BaseDS/srt = v_srt; + + e_base_ds : GeologMeta/BaseDS; + e_base_ds GeologMeta/BaseDS/srt = e_srt; + + v_dsort : GeologMeta/DSort; + v_base_ds GeologMeta/BaseDS/dsort = v_dsort; + + e_dsort : GeologMeta/DSort; + e_base_ds GeologMeta/BaseDS/dsort = e_dsort; + + src_func : GeologMeta/Func; + src_func GeologMeta/Func/theory = target_theory; + src_func GeologMeta/Func/dom = e_dsort; + src_func GeologMeta/Func/cod = v_dsort; + + // NOTE: For a complete example, we'd also need an Instance element + // and Elem elements. For simplicity, we use a simpler predicate structure. + + // Using TruePred for now (matches all, demonstrating structure) + + // -- Query Plan -- + // Schema for E + e_base_schema : BaseSchema; + e_base_schema BaseSchema/srt = e_srt; + + e_schema : Schema; + e_base_schema BaseSchema/schema = e_schema; + + // Wire 1: output of Scan (E elements) + w1 : Wire; + w1 Wire/schema = e_schema; + + // Wire 2: output of Filter (filtered E elements) + w2 : Wire; + w2 Wire/schema = e_schema; + + // Scan operation + scan : ScanOp; + scan ScanOp/srt = e_srt; + scan ScanOp/out = w1; + + scan_op : Op; + scan ScanOp/op = scan_op; + + // Predicate: TruePred (matches all - demonstrates filter structure) + true_pred : TruePred; + pred_elem : Pred; + true_pred TruePred/pred = pred_elem; + + // Filter operation: w1 --[Filter(pred)]--> w2 + filter : FilterOp; + filter FilterOp/in = w1; + filter FilterOp/out = w2; + filter FilterOp/pred = pred_elem; + + filter_op : Op; + filter FilterOp/op = filter_op; +} diff --git a/examples/geolog/solver_demo.geolog b/examples/geolog/solver_demo.geolog new file mode 100644 index 0000000..b8dec99 --- /dev/null +++ b/examples/geolog/solver_demo.geolog @@ -0,0 +1,132 @@ +// Solver Demo: Theories demonstrating the geometric logic solver +// +// Use the :solve command to find instances of these theories: +// :source examples/geolog/solver_demo.geolog +// :solve EmptyModel +// :solve Inhabited +// :solve Inconsistent +// +// The solver uses forward chaining to automatically: +// - Add witness elements for existentials +// - Assert relation tuples +// - Detect unsatisfiability (derivation of False) + +// ============================================================================ +// Theory 1: EmptyModel - Trivially satisfiable with empty carrier +// ============================================================================ +// +// A theory with no axioms is satisfied by the empty structure. +// The solver should report SOLVED immediately with 0 elements. + +theory EmptyModel { + A : Sort; + B : Sort; + f : A -> B; + R : A -> Prop; +} + +// ============================================================================ +// Theory 2: UnconditionalExistential - Requires witness creation +// ============================================================================ +// +// Axiom: forall x : P. |- exists y : P. y R +// +// SUBTLE: This axiom's premise (True) and conclusion (∃y.R(y)) don't mention x! +// So even though there's a "forall x : P", the check happens once for an empty +// assignment. The premise True holds, but ∃y.R(y) doesn't hold for empty P +// (no witnesses). The solver correctly detects this and adds a witness. +// +// This is correct geometric logic semantics! The universal over x doesn't +// protect against empty P because x isn't used in the formulas. + +theory UnconditionalExistential { + P : Sort; + R : P -> Prop; + + // This effectively says "there must exist some y with R(y)" + // because x is unused - the check happens once regardless of |P| + ax : forall x : P. |- exists y : P. y R; +} + +// ============================================================================ +// Theory 3: VacuouslyTrue - Axiom that IS vacuously true for empty carriers +// ============================================================================ +// +// Axiom: forall x : P. |- x R +// +// For every x, assert R(x). When P is empty, there are no x values to check, +// so the axiom is vacuously satisfied. Compare with UnconditionalExistential! + +theory VacuouslyTrue { + P : Sort; + R : P -> Prop; + + // This truly IS vacuously true for empty P because x IS used in the conclusion + ax : forall x : P. |- x R; +} + +// ============================================================================ +// Theory 4: Inconsistent - UNSAT via derivation of False +// ============================================================================ +// +// Axiom: forall x. |- false +// +// For any element x, we derive False. This is immediately UNSAT. +// The solver detects this and reports UNSAT. + +theory Inconsistent { + A : Sort; + + // Contradiction: any element leads to False + ax : forall a : A. |- false; +} + +// ============================================================================ +// Theory 5: ReflexiveRelation - Forward chaining asserts reflexive tuples +// ============================================================================ +// +// Axiom: forall x. |- R(x, x) +// +// For every element x, the pair (x, x) is in relation R. +// The solver will assert R(x, x) for each element added. + +theory ReflexiveRelation { + X : Sort; + R : [a: X, b: X] -> Prop; + + // Reflexivity: every element is related to itself + ax/refl : forall x : X. |- [a: x, b: x] R; +} + +// ============================================================================ +// Theory 6: ChainedWitness - Nested existential body processing +// ============================================================================ +// +// Axiom: forall x. |- exists y. exists z. E(x, y), E(y, z) +// +// For every x, there exist y and z such that E(x,y) and E(y,z). +// Forward chaining creates witnesses and asserts the relations. + +theory ChainedWitness { + N : Sort; + E : [src: N, tgt: N] -> Prop; + + // Chain: every node has a two-step path out + ax/chain : forall x : N. |- exists y : N. exists z : N. [src: x, tgt: y] E, [src: y, tgt: z] E; +} + +// ============================================================================ +// Theory 7: EqualityCollapse - Equation handling via congruence closure +// ============================================================================ +// +// Axiom: forall x, y. |- x = y +// +// All elements of sort X are equal. The solver adds equations to the +// congruence closure and merges equivalence classes. + +theory EqualityCollapse { + X : Sort; + + // All elements are equal + ax/all_equal : forall x : X, y : X. |- x = y; +} diff --git a/examples/geolog/sort_param_simple.geolog b/examples/geolog/sort_param_simple.geolog new file mode 100644 index 0000000..1ba3217 --- /dev/null +++ b/examples/geolog/sort_param_simple.geolog @@ -0,0 +1,31 @@ +// Simpler sort parameter test + +theory (X : Sort) Container { + elem : X; // not a Sort, but an element of X +} + +// Hmm, this doesn't quite work... +// Let me try the actual vision pattern + +theory Base { + A : Sort; + B : Sort; +} + +instance MyBase : Base = { + a1 : A; + a2 : A; + b1 : B; + b2 : B; +} + +// Now try a theory parameterized by an instance +theory (Inst : Base instance) Map { + map : Inst/A -> Inst/B; +} + +// Instance of Map parameterized by MyBase +instance MyMap : MyBase Map = { + a1 map = MyBase/b1; + a2 map = MyBase/b2; +} diff --git a/examples/geolog/todo_list.geolog b/examples/geolog/todo_list.geolog new file mode 100644 index 0000000..aa2cab9 --- /dev/null +++ b/examples/geolog/todo_list.geolog @@ -0,0 +1,44 @@ +// TodoList: A simple relational model for tracking tasks +// +// This demonstrates geolog as a persistent relational database. +// Elements represent tasks, and relations track their status. + +theory TodoList { + // The sort of todo items + Item : Sort; + + // Unary relations for item status (simple arrow syntax) + completed : Item -> Prop; + high_priority : Item -> Prop; + blocked : Item -> Prop; + + // Binary relation for dependencies + depends : [item: Item, on: Item] -> Prop; + + // Axiom: if an item depends on another, either it is blocked + // or the dependency is completed + ax/dep_blocked : forall x : Item, y : Item. + [item: x, on: y] depends |- x blocked \/ y completed; +} + +// Example: An empty todo list ready for interactive use +instance MyTodos : TodoList = { + // Start empty - add items interactively with :add +} + +// Example: A pre-populated todo list +instance SampleTodos : TodoList = { + // Items + buy_groceries : Item; + cook_dinner : Item; + do_laundry : Item; + clean_house : Item; + + // Status: unary relations use simple syntax + buy_groceries completed; + cook_dinner high_priority; + + // Dependencies: cook_dinner depends on buy_groceries + // Mixed syntax: first positional arg maps to 'item' field + [cook_dinner, on: buy_groceries] depends; +} diff --git a/examples/geolog/transitive_closure.geolog b/examples/geolog/transitive_closure.geolog new file mode 100644 index 0000000..7e76309 --- /dev/null +++ b/examples/geolog/transitive_closure.geolog @@ -0,0 +1,77 @@ +// Transitive Closure Example +// +// This example demonstrates the chase algorithm computing transitive +// closure of a relation. We define a Graph theory with Edge and Path +// relations, where Path is the transitive closure of Edge. +// +// Run with: +// cargo run -- examples/geolog/transitive_closure.geolog +// Then: +// :source examples/geolog/transitive_closure.geolog +// :inspect Chain +// :chase Chain +// +// The chase will derive Path tuples for all reachable pairs: +// - Edge(a,b), Edge(b,c), Edge(c,d) as base facts +// - Path(a,b), Path(b,c), Path(c,d) from base axiom +// - Path(a,c), Path(b,d) from one step of transitivity +// - Path(a,d) from two steps of transitivity + +theory Graph { + V : Sort; + + // Direct edges in the graph + Edge : [src: V, tgt: V] -> Prop; + + // Reachability (transitive closure of Edge) + Path : [src: V, tgt: V] -> Prop; + + // Base case: every edge is a path + ax/base : forall x, y : V. + [src: x, tgt: y] Edge |- [src: x, tgt: y] Path; + + // Inductive case: paths compose + ax/trans : forall x, y, z : V. + [src: x, tgt: y] Path, [src: y, tgt: z] Path |- [src: x, tgt: z] Path; +} + +// A linear chain: a -> b -> c -> d +// Chase derives Path tuples from Edge via ax/base and ax/trans. +instance Chain : Graph = chase { + a : V; + b : V; + c : V; + d : V; + + // Edges form a chain + [src: a, tgt: b] Edge; + [src: b, tgt: c] Edge; + [src: c, tgt: d] Edge; +} + +// A diamond: a -> b, a -> c, b -> d, c -> d +// Chase derives all reachable paths. +instance Diamond : Graph = chase { + top : V; + left : V; + right : V; + bottom : V; + + // Two paths from top to bottom + [src: top, tgt: left] Edge; + [src: top, tgt: right] Edge; + [src: left, tgt: bottom] Edge; + [src: right, tgt: bottom] Edge; +} + +// A cycle: a -> b -> c -> a +// Chase derives all reachable paths (full connectivity). +instance Cycle : Graph = chase { + x : V; + y : V; + z : V; + + [src: x, tgt: y] Edge; + [src: y, tgt: z] Edge; + [src: z, tgt: x] Edge; +}