First-order logic with a deterministic transitive closure

Lax485149.DeterministicTransitiveClosure · concepts/Lax485149/DeterministicTransitiveClosure.lean · lax-485149

definition

Loading review…

Natural Language Statement

Definition

The determinization of a transitive-closure specification keeps its modes, arity, source and target formulas, and replaces each transition formula $\varphi_{m,n}(\bar x, \bar y)$ by

\varphi_{m,n}(\bar x, \bar y) \wedge \bigwedge_{m'} \forall \bar z\, \bigl(\varphi_{m,m'}(\bar x, \bar z) \to m' = n \wedge \bar z = \bar y\bigr),

the comparison of modes being resolved statically. In the graph it defines, a node has an outgoing edge exactly when it had a single one in the original graph: the walk follows the forced steps only.

A decision problem $P$ over a vocabulary $L$ is FO(DTC) definable when the determinization of some specification accepts, for every nonempty finite $L$ -structure $A$ and every linear order on $A$ , exactly when $A$ is a yes-instance of $P$ . This is first-order logic with a deterministic transitive closure operator on ordered structures, in the normal form of a single application.

Concept map

4 concepts; 22 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

Show types on hover

1	import Mathlib.ModelTheory.Order
2	import Mathlib.ModelTheory.Semantics
3	import Lax485149.TransitiveClosure
4	import Lax904597.Problems
5	import Lax904597.Interpretations
6
7	/-!
8	---
9	title: First-order logic with a deterministic transitive closure
10	type: definition
11	---
12	The determinization of a transitive-closure specification keeps its modes,
13	arity, source and target formulas, and replaces each transition formula
14	$\varphi_{m,n}(\bar x, \bar y)$ by
15	$\varphi_{m,n}(\bar x, \bar y) \wedge \bigwedge_{m'} \forall \bar z\, \bigl(\varphi_{m,m'}(\bar x, \bar z) \to m' = n \wedge \bar z = \bar y\bigr),$
16
17	the comparison of modes being resolved statically. In the graph it defines,
18	a node has an outgoing edge exactly when it had a single one in the original
19	graph: the walk follows the forced steps only.
20
21	A decision problem $P$ over a vocabulary $L$ is FO(DTC) definable when the
22	determinization of some specification accepts, for every nonempty finite
23	$L$ -structure $A$ and every linear order on $A$ , exactly when $A$ is a
24	yes-instance of $P$ . This is first-order logic with a deterministic
25	transitive closure operator on ordered structures, in the normal form of a
26	single application.
27	-/
28
29	namespace Lax485149.DeterministicTransitiveClosure
30
31	open Lax485149.TransitiveClosure Lax904597.Problems
32
33	open FirstOrder
34
35	open Language Structure
36
37	namespace TCSpec
38
39	section Det
40
41	variable {L : Language.{0, 0}} (spec : TCSpec L)
42
43	/-- The renaming used by the uniqueness clause: the transition formula is
44	re-read with its first tuple still the current one and its second tuple the
45	freshly quantified `z̄`. -/
46	def detVar : Fin spec.k ⊕ Fin spec.k → (Fin spec.k ⊕ Fin spec.k) ⊕ Fin spec.k :=
47	Sum.elim (fun i => Sum.inl (Sum.inl i)) Sum.inr
48
49	open Classical in
50	/-- The determinized transition formula at a pair of modes: this step, and
51	no other step out of the current node. The competing successors are quantified
52	as a tuple `z̄` and a mode `m'`; the mode is compared statically, so the
53	uniqueness clause has one conjunct per mode, asserting `z̄ = ȳ` at the intended
54	one and refuting the step at every other. -/
55	noncomputable def detStep (m n : spec.Mode) :
56	(L.sum Language.order).Formula (Fin spec.k ⊕ Fin spec.k) :=
57	spec.step m n ⊓
58	Formula.iInf fun m' : spec.Mode =>
59	Formula.iAlls (Fin spec.k)
60	(((spec.step m m').relabel (detVar spec)).imp
61	(if m' = n then
62	Formula.iInf fun i : Fin spec.k =>
63	Term.equal (Term.var (Sum.inr i)) (Term.var (Sum.inl (Sum.inr i)))
64	else ⊥))
65
66	/-- The deterministic reading of a specification: the same modes, arity and
67	endpoints, with the transition formula replaced by its determinization.
68
69	Marked `@[reducible]` so that the modes and the arity of `spec.det` are those of
70	`spec` transparently: a node of the deterministic reading is a node, and
71	numerals at `Fin spec.det.k` elaborate as they do at `Fin spec.k`. -/
72	@[reducible]
73	noncomputable def det : TCSpec L where
74	Mode := spec.Mode
75	k := spec.k
76	step := detStep spec
77	src := spec.src
78	tgt := spec.tgt
79
80	end Det
81
82	end TCSpec
83
84	/-- A decision problem is FO(DTC) definable if, on nonempty finite ordered
85	structures, it is defined by a single deterministic transitive closure:
86	there is a `TCSpec` whose accepting nodes are reachable from its starting
87	nodes along its determinization exactly on the yes-instances.
88
89	As for `TCDefinable`, the equivalence is required for every linear order on
90	the universe, so this is order-invariant FO(DTC) definability. -/
91	def DTCDefinable {L : Language.{0, 0}} [L.IsRelational] (P : DecisionProblem L) : Prop :=
92	∃ spec : TCSpec L,
93	∀ (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A],
94	P A ↔ (TCSpec.det spec).Accepts A
95
96	end Lax485149.DeterministicTransitiveClosure
97

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

Loading discussion…

Lax Lean Archive

First-order logic with a deterministic transitive closure

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments