Problems given by a property of structures
Lax624099.Problems · concepts/Lax624099/Problems.lean · lax-624099
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
The decision problems of the NP core are bundled with a proof that they do not distinguish isomorphic structures. For the problems of this submission the bundling is done once and for all: the problem given by a property of structures has as yes-instances the structures isomorphic to one satisfying , which is invariant by construction. When is itself invariant, as every property here is, this is the problem whose yes-instances are exactly the structures satisfying ; that equivalence is stated, problem by problem, beside each definition.
Concept map
Lean source view on GitHub
| 1 | import Lax904597.Problems |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: Problems given by a property of structures |
| 6 | type: definition |
| 7 | --- |
| 8 | The decision problems of the NP core are bundled with a proof that they do |
| 9 | not distinguish isomorphic structures. For the problems of this submission |
| 10 | the bundling is done once and for all: the problem given by a property of |
| 11 | structures has as yes-instances the structures isomorphic to one satisfying |
| 12 | , which is invariant by construction. When is itself invariant, as |
| 13 | every property here is, this is the problem whose yes-instances are exactly |
| 14 | the structures satisfying ; that equivalence is stated, problem by |
| 15 | problem, beside each definition. |
| 16 | -/ |
| 17 | |
| 18 | namespace Lax624099.Problems |
| 19 | |
| 20 | open FirstOrder FirstOrder.Language Lax904597.Problems |
| 21 | |
| 22 | /-- The decision problem whose yes-instances are the structures isomorphic to |
| 23 | one satisfying `P`. -/ |
| 24 | def DecisionProblem.ofPred {L : Language.{0, 0}} [L.IsRelational] |
| 25 | (P : ∀ (A : Type) [L.Structure A], Prop) : DecisionProblem L where |
| 26 | Holds := fun A _ => ∃ (B : Type) (i : L.Structure B) (_ : @Language.Equiv L B A i _), @P B i |
| 27 | iso_invariant := fun e => |
| 28 | ⟨fun ⟨B, i, f, h⟩ => ⟨B, i, e.comp f, h⟩, fun ⟨B, i, f, h⟩ => ⟨B, i, e.symm.comp f, h⟩⟩ |
| 29 | |
| 30 | end Lax624099.Problems |
| 31 |
Builds on
Used by
Lax624099.CodeHaltingLax624099.CodeHaltingInvarianceLax624099.CodehaltRECompleteLax624099.FiniteSatisfiabilityLax624099.FiniteSatisfiabilityInvarianceLax624099.FinsatRECompleteLax624099.HaltingLax624099.HaltingInvarianceLax624099.HaltingUndecidableLax624099.HaltRECompleteLax624099.NPSubsetRELax624099.PcpRECompleteLax624099.PcpUndecidableLax624099.PostCorrespondenceLax624099.PostCorrespondenceInvarianceLax624099.REClosureLax624099.ReductionsComputableLax624099.REFiniteLax624099.REHardUndecidableLax624099.REIsRecursivelyEnumerableLax624099.RENeCoRELax624099.Trakhtenbrot
From Mathlib
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments