Reading the kernel of an ∃SO[new] definition, position by position #
The encoded sentence the RE-hardness reduction produces has one node per
(subformula position, polarity) of the kernel φ, so the defining formulas of
the interpretation have to answer two questions about a position:
- what does the kernel say there? –
DescriptiveComplexity.FinSat.kernelNode, which reads off the constructor at the position together with the data the node needs: the de Bruijn levels of the arguments (DescriptiveComplexity.FinSat.termLevel), the relation symbol of an atom, the level a quantifier binds; - which positions are its children, and does the polarity flip there? –
DescriptiveComplexity.FinSat.kidOf,some trueat the premise of an implication (the one place negation normal form flips a polarity),some falseat its conclusion and under a quantifier,noneelsewhere.
Both are computed by recursion on φ, which is what a defining formula must do:
the positions of a variable formula cannot be matched on directly (the
litF/isClauseF idiom of DescriptiveComplexity.Problems.Sat.TseitinFormulas).
Neither mentions the instance, so both are pure syntax – the reduction reads the
instance only in the tuple coordinates of its tags.
DescriptiveComplexity.FinSat.nodeSize_lt_of_kidOf is what this buys for
well-formedness: a child position carries a strictly smaller subformula, so the
parse DAG of the image descends along the order of its syntax.
Levels are ℕ, not Fin of anything: an argument at a position of context
length m has level below m ≤ maxCtx φ, and the tag dbvar l carries
l : Fin (maxCtx φ), so comparing the two as naturals is exactly right and
needs no cast through the changing bound of a recursion.
The children of a position #
The children of a position, with the polarity flip: some true at the
premise of an implication – where negation normal form turns f₁ → f₂ into
¬f₁ ∨ f₂ – some false at its conclusion and at the body of a quantifier,
and none when q is not a child of p at all.
Equations
- DescriptiveComplexity.FinSat.kidOf FirstOrder.Language.BoundedFormula.falsum x✝¹ x✝ = none
- DescriptiveComplexity.FinSat.kidOf (FirstOrder.Language.BoundedFormula.equal t₁ t₂) x✝¹ x✝ = none
- DescriptiveComplexity.FinSat.kidOf (FirstOrder.Language.BoundedFormula.rel R ts) x✝¹ x✝ = none
- DescriptiveComplexity.FinSat.kidOf (f₁.imp f₂) (Sum.inl val) (Sum.inr (Sum.inl q₁)) = if DescriptiveComplexity.Tseitin.isRootB f₁ q₁ = true then some true else none
- DescriptiveComplexity.FinSat.kidOf (f₁.imp f₂) (Sum.inl val) (Sum.inr (Sum.inr q₂)) = if DescriptiveComplexity.Tseitin.isRootB f₂ q₂ = true then some false else none
- DescriptiveComplexity.FinSat.kidOf (f₁.imp f₂) (Sum.inr (Sum.inl p₁)) (Sum.inr (Sum.inl q₁)) = DescriptiveComplexity.FinSat.kidOf f₁ p₁ q₁
- DescriptiveComplexity.FinSat.kidOf (f₁.imp f₂) (Sum.inr (Sum.inr p₂)) (Sum.inr (Sum.inr q₂)) = DescriptiveComplexity.FinSat.kidOf f₂ p₂ q₂
- DescriptiveComplexity.FinSat.kidOf (f₁.imp f₂) x✝¹ x✝ = none
- DescriptiveComplexity.FinSat.kidOf f.all (Sum.inl val) (Sum.inr q') = if DescriptiveComplexity.Tseitin.isRootB f q' = true then some false else none
- DescriptiveComplexity.FinSat.kidOf f.all (Sum.inr p') (Sum.inr q') = DescriptiveComplexity.FinSat.kidOf f p' q'
- DescriptiveComplexity.FinSat.kidOf f.all x✝¹ x✝ = none
Instances For
Dependency graph
The three children the translation actually uses.
Dependency graph
Dependency graph
Dependency graph
The children of a position of a subformula stay inside that subformula: what lets an induction over subformulas see all the children a node of the whole kernel has.
Dependency graph
Dependency graph
Dependency graph
The children of the root of an implication are the roots of its two sides, and the children of the root of a quantifier the root of its body: what an induction over subformulas descends along.
Dependency graph
Dependency graph
A child carries a strictly smaller subformula. This is what makes the
parse DAG of the image acyclic, and it is all the order of the syntax is asked
to witness (DescriptiveComplexity.FinSat.IsWF.child_lt).
Dependency graph
What the kernel says at a position #
The de Bruijn level a term denotes, when it is a variable at all: none for
a function application, which the relational milestone of the reduction excludes
and the term layer translates by its graph (the junk-value hazard).
Equations
Instances For
Dependency graph
What the kernel says at a position: the constructor there, with the data
the corresponding node of the encoded sentence needs. The three kinds of atom
are separated, because the encoded sentence may name only the relation
variables – an atom of the instance's vocabulary, and the marker old, are
translated away into a disjunction over the tuples where they hold.
- fls
{L : FirstOrder.Language}
{B : SOBlock}
: KernelNode L B
Falsity.
- eqLit
{L : FirstOrder.Language}
{B : SOBlock}
(x y : Option ℕ)
: KernelNode L B
An equality of two terms.
- blockAtom
{L : FirstOrder.Language}
{B : SOBlock}
{k : ℕ}
(r : B.lang.Relations k)
(args : Fin k → Option ℕ)
: KernelNode L B
An atom of a relation variable of the block: a genuine atom of the encoded sentence.
- inputAtom
{L : FirstOrder.Language}
{B : SOBlock}
{k : ℕ}
(r : L.Relations k)
(args : Fin k → Option ℕ)
: KernelNode L B
An atom of the instance's vocabulary, which the encoded sentence must not mention.
- oldAtom
{L : FirstOrder.Language}
{B : SOBlock}
(x : Option ℕ)
: KernelNode L B
The marker of the original elements, likewise.
- impl
{L : FirstOrder.Language}
{B : SOBlock}
: KernelNode L B
An implication.
- quant
{L : FirstOrder.Language}
{B : SOBlock}
(lvl : ℕ)
: KernelNode L B
A quantifier, binding the given de Bruijn level.
Instances For
Dependency graph
Reading a position of the kernel, by recursion on the kernel: a defining formula cannot match on the positions of a variable formula.
Equations
- One or more equations did not get rendered due to their size.
- DescriptiveComplexity.FinSat.kernelNode FirstOrder.Language.BoundedFormula.falsum x✝ = DescriptiveComplexity.FinSat.KernelNode.fls
- DescriptiveComplexity.FinSat.kernelNode (f₁.imp f₂) (Sum.inl val) = DescriptiveComplexity.FinSat.KernelNode.impl
- DescriptiveComplexity.FinSat.kernelNode (f₁.imp f₂) (Sum.inr (Sum.inl q)) = DescriptiveComplexity.FinSat.kernelNode f₁ q
- DescriptiveComplexity.FinSat.kernelNode (f₁.imp f₂) (Sum.inr (Sum.inr q)) = DescriptiveComplexity.FinSat.kernelNode f₂ q
- DescriptiveComplexity.FinSat.kernelNode f.all (Sum.inl val) = DescriptiveComplexity.FinSat.KernelNode.quant x✝¹
- DescriptiveComplexity.FinSat.kernelNode f.all (Sum.inr q) = DescriptiveComplexity.FinSat.kernelNode f q
Instances For
Dependency graph
Dependency graph
Dependency graph
The atoms of the relation variables #
The three accessors an atom of the encoded sentence is read through – its relation symbol, its arity, and the de Bruijn level of each of its arguments – together with what the shape conditions of well-formedness ask of them: an argument sits below the arity, the arity is the one the block declares, and (in a relational vocabulary) every position below the arity does carry a level.
The relation variable of the block a position carries, if it carries one.
Equations
- DescriptiveComplexity.FinSat.symOf f q = match DescriptiveComplexity.FinSat.kernelNode f q with | DescriptiveComplexity.FinSat.KernelNode.blockAtom r args => some ↑r | x => none
Instances For
Dependency graph
The arity of the atom a position carries, 0 when it carries none.
Equations
- DescriptiveComplexity.FinSat.arityOf f q = match DescriptiveComplexity.FinSat.kernelNode f q with | DescriptiveComplexity.FinSat.KernelNode.blockAtom r args => k | x => 0
Instances For
Dependency graph
The de Bruijn level of the j-th argument of that atom.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Dependency graph
The arity is the one the block declares: the relation symbols of the block are its indices, tagged by their arity.
Dependency graph
The dimension is wide enough for an atom of a relation variable too: its arity is one of the arities occurring in the kernel.
Dependency graph
An argument sits below the arity.
Dependency graph
The de Bruijn level a term denotes is one of the context: in a relational vocabulary every term is a variable.
Dependency graph
The arity of an atom the encoded sentence must not mention: one of the
input vocabulary, or the marker old, both of which the translation replaces by
a disjunction over the tuples where they hold.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Dependency graph
The dimension of the reduction is wide enough for such an atom: its arity is one of the arities occurring in the kernel.
Dependency graph
Every position below the arity carries a level, in a relational
vocabulary – and the level is one of the de Bruijn levels of the kernel. This is
what lets the image of the reduction give an atom an argument at each position
of its signature (DescriptiveComplexity.FinSat.IsWF.arg_tot).
Dependency graph
The value of a term of the kernel, when it is a variable: the context tuple at its de Bruijn level.
Dependency graph
Subformulas, and their positions inside the kernel #
Tseitin.Gates – the recursion the encoded sentence has to compute – is defined
by recursion on the formula with the node valuation restricted along each
descent. The induction that proves the image satisfies it must therefore be
generalized over an embedding of a subformula's positions into the kernel's,
carrying the three facts that make the kernel's reading of an embedded position
the same as the subformula's: what the kernel says there, which positions are
its children, and – the one with content – that those children are themselves
embedded, so that a clause quantifying over all the children a node has in the
kernel collapses to the subformula.
All three are definitional at each of the three descents, because that is
exactly how DescriptiveComplexity.FinSat.kernelNode and
DescriptiveComplexity.FinSat.kidOf are defined; the third rests on the range
lemmas above.
A subformula of the kernel, with its positions embedded in the kernel's.
- emb {m : ℕ} : Tseitin.NodeAt f m → Tseitin.NodeAt φ m
Where a position of the subformula sits in the kernel; the context length is the same.
The kernel says at an embedded position what the subformula says.
- kid {m : ℕ} (q : Tseitin.NodeAt f m) {m' : ℕ} (q' : Tseitin.NodeAt f m') : kidOf φ (self.emb q) (self.emb q') = kidOf f q q'
The child relation is the same.
- kid_range {m : ℕ} (q : Tseitin.NodeAt f m) {m' : ℕ} (r : Tseitin.NodeAt φ m') {b : Bool} : kidOf φ (self.emb q) r = some b → ∃ (q' : Tseitin.NodeAt f m'), r = self.emb q'
Every child an embedded position has in the kernel is itself embedded.
Instances For
Dependency graph
The kernel is a subformula of itself.
Equations
- DescriptiveComplexity.FinSat.SubEmb.refl φ = { emb := fun {x : ℕ} (q : DescriptiveComplexity.Tseitin.NodeAt φ x) => q, node := ⋯, kid := ⋯, kid_range := ⋯ }
Instances For
Dependency graph
The premise of an implication.
Equations
Instances For
Dependency graph
The conclusion of an implication.
Equations
Instances For
Dependency graph
The body of a quantifier.
Equations
Instances For
Dependency graph
What the children of the root of an embedded subformula are, in the kernel: the three facts the induction over subformulas needs, one per shape.
The root of an embedded leaf – falsity, an equality or an atom – has no children in the kernel.
Dependency graph
The children of the root of an embedded implication are the roots of its two
sides, the premise at some true – where negation normal form flips the
polarity – and the conclusion at some false.
Dependency graph
The only child of the root of an embedded quantifier is the root of its body.