Term graphs: relationalizing a term's value (Craig Layer 3, Unit 3)

The graph formula of a term: termGraph t y asserts, in the relationalized language graphLanguage L, that the value of the L-term t is (the value of) the variable term y. Nested applications are flattened through auxiliary bound variables — one block of k fresh variables per k-ary function application, bound by existsBlock — with each argument's value pinned by its own recursive graph formula and the application itself by one graph atom G_f(y⃗, y).

Design

The recursion is context-polymorphic (termGraphAux): instead of relabeling already-built graph formulas when the bound context grows, the auxiliary carries a variable embedding ρ : β → (graphLanguage L).Term (α ⊕ Fin m) of the term's variables into the current context and a proposed output term y. Recursive calls enlarge m by the function arity while still structurally recurring on a genuine subterm, and existsBlock (Unit 2) handles all environment growth uniformly. Arity 0 (constants) is the same construction with an empty witness block — no special case.

The semantics is oriented term value equals output — matching the landed graph-relation definition funMap f args = output (graphExpansion_relMap_graph) — so no symmetry rewrites are ever needed.

Main Results

• realize_termGraphAux: the stronger context-polymorphic semantics, (termGraphAux t ρ y).Realize v xs ↔ t.realize (fun z => (ρ z).realize (Sum.elim v xs)) = y.realize (Sum.elim v xs) over the graph expansion.
• realize_termGraph: the public form, t.realize (Sum.elim v xs) = y.realize (Sum.elim v xs).
• relationsIn_termGraph: the graph formula's relation occurrences are exactly the graphRelSym-image of t.functionsIn — in particular no base relations occur (relationsIn_termGraph_inter_base), and no function symbols occur at all (functionsIn_termGraph, the language is relational).
• The nested-term pilot f(g(x), h(c)) (genuinely nested, includes a 0-ary application).

Context lifting and witness variables

def FirstOrder.Language.graphTermLift {L : Language} {α : Type} {m : ℕ} (k : ℕ) (u : L.graphLanguage.Term (α ⊕ Fin m)) : L.graphLanguage.Term (α ⊕ Fin (m + k))

Lift a graph-language term along the bound-context extension m → m + k (the existing context keeps the first m coordinates).

Equations

• FirstOrder.Language.graphTermLift k u = FirstOrder.Language.Term.relabel (Sum.map id (Fin.castAdd k)) u

def FirstOrder.Language.graphWitnessVar {L : Language} {α : Type} (m : ℕ) {k : ℕ} (i : Fin k) : L.graphLanguage.Term (α ⊕ Fin (m + k))

The i-th auxiliary witness variable of a fresh block of k bound variables appended to a context of size m.

Equations

• FirstOrder.Language.graphWitnessVar m i = FirstOrder.Language.var (Sum.inr (Fin.natAdd m i))

The term-graph formula

def FirstOrder.Language.termGraphAux {L : Language} {α β : Type} {m : ℕ} : L.Term β → (β → L.graphLanguage.Term (α ⊕ Fin m)) → L.graphLanguage.Term (α ⊕ Fin m) → L.graphLanguage.BoundedFormulaω α m

The context-polymorphic term-graph formula: termGraphAux t ρ y asserts that the value of the L-term t — its variables read through the embedding ρ into the current context — is the value of y. A variable is an equality atom; an application f(t₀, …, t_{k-1}) extends the context by k witness variables, pins each argument's value with a recursive graph formula, adds the graph atom G_f(y⃗, y), and existentially closes the witness block.

Equations

• One or more equations did not get rendered due to their size.
• FirstOrder.Language.termGraphAux (FirstOrder.Language.var z) x✝¹ x✝ = FirstOrder.Language.BoundedFormulaω.equal (x✝¹ z) x✝

def FirstOrder.Language.termGraph {L : Language} {α : Type} {m : ℕ} (t : L.Term (α ⊕ Fin m)) (y : L.graphLanguage.Term (α ⊕ Fin m)) : L.graphLanguage.BoundedFormulaω α m

The term-graph formula over the ambient context, via the identity variable embedding: termGraph t y asserts in graphLanguage L that the value of t is the value of y.

Equations

• FirstOrder.Language.termGraph t y = FirstOrder.Language.termGraphAux t FirstOrder.Language.var y

Semantics over the graph expansion

@[simp]

theorem FirstOrder.Language.realize_graphTermLift {L : Language} {α : Type} {m : ℕ} {M : Type} [L.Structure M] {k : ℕ} (u : L.graphLanguage.Term (α ⊕ Fin m)) (v : α → M) (xs : Fin m → M) (ws : Fin k → M) : Term.realize (Sum.elim v (Fin.append xs ws)) (graphTermLift k u) = Term.realize (Sum.elim v xs) u

@[simp]

theorem FirstOrder.Language.realize_graphWitnessVar {L : Language} {α : Type} {m : ℕ} {M : Type} [L.Structure M] {k : ℕ} (i : Fin k) (v : α → M) (xs : Fin m → M) (ws : Fin k → M) : Term.realize (Sum.elim v (Fin.append xs ws)) (graphWitnessVar m i) = ws i

theorem FirstOrder.Language.realize_termGraphAux {L : Language} {α β M : Type} [L.Structure M] {m : ℕ} (t : L.Term β) (ρ : β → L.graphLanguage.Term (α ⊕ Fin m)) (y : L.graphLanguage.Term (α ⊕ Fin m)) (v : α → M) (xs : Fin m → M) : (termGraphAux t ρ y).Realize v xs ↔ Term.realize (fun (z : β) => Term.realize (Sum.elim v xs) (ρ z)) t = Term.realize (Sum.elim v xs) y

Auxiliary semantics (the stronger, context-polymorphic form): over the graph expansion, termGraphAux t ρ y holds iff the value of t — its variables read through ρ — equals the value of y. Oriented term value equals output, matching graphExpansion_relMap_graph.

theorem FirstOrder.Language.realize_termGraph {L : Language} {α : Type} {m : ℕ} {M : Type} [L.Structure M] (t : L.Term (α ⊕ Fin m)) (y : L.graphLanguage.Term (α ⊕ Fin m)) (v : α → M) (xs : Fin m → M) : (termGraph t y).Realize v xs ↔ Term.realize (Sum.elim v xs) t = Term.realize (Sum.elim v xs) y

Public semantics: over the graph expansion, termGraph t y holds iff the value of t equals the value of y in the ambient environment.

The nested-term pilot: f(g(x), h(c))

Genuinely nested arguments (each argument is itself an application) and a 0-ary application (c), all through the same construction — the acceptance gate for the unit.

Occurrence identities

theorem FirstOrder.Language.relationsIn_termGraphAux {L : Language} {α β : Type} {m : ℕ} (t : L.Term β) (ρ : β → L.graphLanguage.Term (α ⊕ Fin m)) (y : L.graphLanguage.Term (α ⊕ Fin m)) : (termGraphAux t ρ y).relationsIn = L.graphRelSym '' t.functionsIn

The relation symbols of the auxiliary term-graph formula are exactly the graph relations of the term's function symbols — independent of the embedding ρ and the output y (graph-language terms are pure variables and contribute nothing).

theorem FirstOrder.Language.relationsIn_termGraph {L : Language} {α : Type} {m : ℕ} (t : L.Term (α ⊕ Fin m)) (y : L.graphLanguage.Term (α ⊕ Fin m)) : (termGraph t y).relationsIn = L.graphRelSym '' t.functionsIn

The relation symbols of termGraph t y are exactly the graph relations of t's function symbols.

theorem FirstOrder.Language.relationsIn_termGraph_inter_base {L : Language} {α : Type} {m : ℕ} (t : L.Term (α ⊕ Fin m)) (y : L.graphLanguage.Term (α ⊕ Fin m)) (R : Set ((n : ℕ) × L.Relations n)) : (termGraph t y).relationsIn ∩ L.baseRelSym '' R = ∅

No base relation occurs in a term-graph formula.

theorem FirstOrder.Language.functionsIn_termGraph {L : Language} {α : Type} {m : ℕ} (t : L.Term (α ⊕ Fin m)) (y : L.graphLanguage.Term (α ⊕ Fin m)) : (termGraph t y).functionsIn = ∅

No function symbol occurs in a term-graph formula (the graph language is relational).