Lax Lean Archive

The classes RE and co-RE

Lax624099.ClassRE · concepts/Lax624099/ClassRE.lean · lax-624099

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    RE is the class of decision problems definable in existential second-order logic with value invention, with the cofinal hardness of the NP core: a problem is RE-hard when every problem it reduces to, by a relativized ordered first-order reduction, is reduced to by every problem of RE. The complement of a decision problem has the no-instances of the problem as yes-instances, and co-RE is the class of problems whose complement is in RE. RE-completeness is membership together with RE-hardness.

    Concept map
    7 concepts; 18 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Lax904597.Problems
    2import Lax904597.Classes
    3import Lax624099.ValueInvention
    4
    5/-!
    6---
    7title: The classes RE and co-RE
    8type: definition
    9---
    10RE is the class of decision problems definable in existential second-order
    11logic with value invention, with the cofinal hardness of the NP core: a
    12problem is RE-hard when every problem it reduces to, by a relativized ordered
    13first-order reduction, is reduced to by every problem of RE. The complement
    14of a decision problem has the no-instances of the problem as yes-instances,
    15and co-RE is the class of problems whose complement is in RE. RE-completeness
    16is membership together with RE-hardness.
    17-/
    18
    19namespace Lax624099.ClassRE
    20
    21open Lax904597.Problems Lax904597.Classes Lax624099.ValueInvention
    22
    23open FirstOrder
    24
    25open Language
    26
    27/-- The complement of a decision problem: its yes-instances are the
    28no-instances of `P`. -/
    29def DecisionProblem.compl {L : Language.{0, 0}} [L.IsRelational]
    30 (P : DecisionProblem L) :
    31 DecisionProblem L where
    32 Holds := fun A inst => ¬@DecisionProblem.Holds L _ P A inst
    33 iso_invariant := fun e => not_congr (P.iso_invariant e)
    34
    35/-- **RE**, the recursively enumerable problems: the class of the
    36`∃SO[new]`-definable problems, with cofinal hardness. -/
    37noncomputable def RE : ComplexityClass :=
    38 ComplexityClass.ofMem fun P => SigmaSONewDefinable P
    39
    40/-- **co-RE**: the problems whose complement is recursively enumerable. -/
    41noncomputable def coRE : ComplexityClass :=
    42 ComplexityClass.ofMem fun P => SigmaSONewDefinable (DecisionProblem.compl P)
    43
    44end Lax624099.ClassRE
    45
    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…