Alternating logarithmic-time machines

Lax895169.LogTimeMachines · concepts/Lax895169/LogTimeMachines.lean · lax-895169

definition

Loading review…

Natural Language Statement

Definition

A machine over a vocabulary $L$ has a list of registers, each holding an element of the universe, that is, an address of about $\log n$ bits, and each filled by one of two players, existential or universal, in the order of the list. It then runs a deterministic test of the tuple of registers, a Boolean combination of three kinds of operations: a query, an atom of $L$ at a tuple of registers, which is the random access to the input; a read, the bit of one register at the position named by another; and a sweep, one pass over the bit positions from the lowest to the highest by a finite automaton that reads, at each position, one bit of the rank of each register. No operation evaluates a numeric predicate.

The machine accepts a finite linearly ordered $L$ -structure when the players, filling the registers in order, leave a tuple passing the test. A decision problem is decidable in logarithmic time with constantly many alternations when some machine accepts, for every nonempty finite $L$ -structure and every linear order on it, exactly the yes-instances. The number of alternations is fixed by the machine, so this is the logarithmic-time hierarchy of Sipser, the union of the classes $\Sigma_k$ -TIME( $\log n$ ).

Concept map

3 concepts; 7 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 Lax904597.Problems
4	import Lax895169.BitPredicate
5
6	/-!
7	---
8	title: Alternating logarithmic-time machines
9	type: definition
10	---
11	A machine over a vocabulary $L$ has a list of registers, each holding an
12	element of the universe, that is, an address of about $\log n$ bits, and
13	each filled by one of two players, existential or universal, in the order
14	of the list. It then runs a deterministic test of the tuple of registers, a
15	Boolean combination of three kinds of operations: a query, an atom of $L$
16	at a tuple of registers, which is the random access to the input; a read,
17	the bit of one register at the position named by another; and a sweep, one
18	pass over the bit positions from the lowest to the highest by a finite
19	automaton that reads, at each position, one bit of the rank of each
20	register. No operation evaluates a numeric predicate.
21
22	The machine accepts a finite linearly ordered $L$ -structure when the
23	players, filling the registers in order, leave a tuple passing the test. A
24	decision problem is decidable in logarithmic time with constantly many
25	alternations when some machine accepts, for every nonempty finite
26	$L$ -structure and every linear order on it, exactly the yes-instances. The
27	number of alternations is fixed by the machine, so this is the
28	logarithmic-time hierarchy of Sipser, the union of the classes
29	$\Sigma_k$ -TIME( $\log n$ ).
30	-/
31
32	namespace Lax895169.LogTimeMachines
33
34	open Lax895169.BitPredicate Lax904597.Problems
35
36	open FirstOrder
37
38	open Language Structure
39
40	/-- A Boolean expression over bit variables: what a sweep computes in one step,
41	and what its acceptance condition is. Expressions rather than functions, so that
42	the translation into a formula is a recursion rather than an enumeration of a
43	truth table. -/
44	inductive BitExpr (V : Type) where
45	/-- A bit variable. -/
46	\| var (v : V) : BitExpr V
47	/-- The constant `true`. -/
48	\| tt : BitExpr V
49	/-- The constant `false`. -/
50	\| ff : BitExpr V
51	/-- Negation. -/
52	\| not (e : BitExpr V) : BitExpr V
53	/-- Conjunction. -/
54	\| and (e f : BitExpr V) : BitExpr V
55	/-- Disjunction. -/
56	\| or (e f : BitExpr V) : BitExpr V
57
58	namespace BitExpr
59
60	variable {V : Type}
61
62	/-- The value of an expression under a `Bool`-valued assignment. -/
63	def eval (val : V → Bool) : BitExpr V → Bool
64	\| .var v => val v
65	\| .tt => true
66	\| .ff => false
67	\| .not e => !(e.eval val)
68	\| .and e f => e.eval val && f.eval val
69	\| .or e f => e.eval val \|\| f.eval val
70
71	end BitExpr
72
73	/-- A sweep: one pass over the bit positions of the universe, from the
74	lowest to the highest, by a finite automaton with `σ` state bits reading, at
75	each position, one bit of each of the `ρ` registers. -/
76	structure Sweep (ρ : ℕ) where
77	/-- The number of state bits. -/
78	σ : ℕ
79	/-- The state before the lowest position. -/
80	init : Fin σ → Bool
81	/-- The next state: one Boolean expression per state bit, over the old state
82	and the register bits at the current position. -/
83	step : Fin σ → BitExpr (Fin σ ⊕ Fin ρ)
84	/-- The acceptance condition, read from the state after the last position. -/
85	acc : BitExpr (Fin σ)
86
87	namespace Sweep
88
89	variable {ρ : ℕ} {A : Type} [LinearOrder A] [Finite A]
90
91	/-- The state of a sweep before position `i`: the automaton starts in its
92	initial state and takes one step per position, reading the bits of the
93	registers there. -/
94	noncomputable def state (S : Sweep ρ) (x : Fin ρ → A) : ℕ → (Fin S.σ → Bool)
95	\| 0 => S.init
96	\| i + 1 => fun j => (S.step j).eval
97	(Sum.elim (state S x i) fun k => (orank (x k)).testBit i)
98
99	/-- A sweep accepts when its acceptance condition holds of the state left
100	after the last bit position. -/
101	def Accepts (S : Sweep ρ) (x : Fin ρ → A) : Prop :=
102	S.acc.eval (S.state x (posCount A)) = true
103
104	end Sweep
105
106	/-- The deterministic base of a machine: a Boolean combination of sweeps and
107	of queries to the instance. Its cost is a constant number of passes over the bit
108	positions, hence `O(log n)` steps; nothing here evaluates a numeric predicate. -/
109	inductive BaseTest (L : Language.{0, 0}) (ρ : ℕ) where
110	/-- Run a sweep on the registers. -/
111	\| sweep (S : Sweep ρ) : BaseTest L ρ
112	/-- Read a bit: the bit of register `x` at the position named by register
113	`i`. The addressing the model has over its own registers, and the one base
114	operation that is not a pass over the positions. -/
115	\| bit (i x : Fin ρ) : BaseTest L ρ
116	/-- Query the instance: an input relation at a tuple of registers. -/
117	\| query {a : ℕ} (R : L.Relations a) (arg : Fin a → Fin ρ) : BaseTest L ρ
118	/-- Negation. -/
119	\| not (t : BaseTest L ρ) : BaseTest L ρ
120	/-- Conjunction. -/
121	\| and (t u : BaseTest L ρ) : BaseTest L ρ
122	/-- Disjunction. -/
123	\| or (t u : BaseTest L ρ) : BaseTest L ρ
124
125	namespace BaseTest
126
127	variable {L : Language.{0, 0}} {ρ : ℕ}
128
129	/-- What a base test says of a tuple of register values. -/
130	def Holds {A : Type} [L.Structure A] [LinearOrder A] [Finite A] :
131	BaseTest L ρ → (Fin ρ → A) → Prop
132	\| .sweep S, x => S.Accepts x
133	\| .bit i y, x => BitIx (x i) (x y)
134	\| .query R arg, x => RelMap R fun t => x (arg t)
135	\| .not t, x => ¬ t.Holds x
136	\| .and t u, x => t.Holds x ∧ u.Holds x
137	\| .or t u, x => t.Holds x ∨ u.Holds x
138
139	end BaseTest
140
141	/-- An alternating machine with a logarithmic clock: a list of registers,
142	each filled by one of the two players, and a deterministic bit-level test of the
143	tuple they leave behind. Registers are filled in order, `pol i` telling which
144	player fills the `i`-th; the number of alternations is the number of changes
145	of polarity along the list. -/
146	structure LTMachine (L : Language.{0, 0}) where
147	/-- The number of registers, that is, of guessed addresses. -/
148	regs : ℕ
149	/-- Who fills each register: `true` existentially, `false` universally. -/
150	pol : Fin regs → Bool
151	/-- The deterministic base test. -/
152	base : BaseTest L regs
153
154	/-- The machine accepts the instance when the two players, filling the
155	registers in order, leave a tuple passing the base test. -/
156	def LTMachine.Accepts {L : Language.{0, 0}} (M : LTMachine L) (A : Type) [L.Structure A]
157	[LinearOrder A] [Finite A] : Prop :=
158	prefixHolds (A := A) M.regs M.pol fun x => M.base.Holds x
159
160	/-- A problem is decidable in constant-alternation logarithmic time when one
161	machine decides it on every nonempty finite ordered structure. -/
162	def LTDecidable {L : Language.{0, 0}} [L.IsRelational] (P : DecisionProblem L) : Prop :=
163	∃ M : LTMachine L, ∀ (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A],
164	P A ↔ M.Accepts A
165
166	end Lax895169.LogTimeMachines
167

Builds on

Used by

From Mathlib

Discussion

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

Loading discussion…

Lax Lean Archive

Alternating logarithmic-time machines

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments