Module functions

Source

Expand description

Auto-generated module

🤖 Generated with SplitRS

Functions§

ac0_class_ty: AC0 circuit class: constant depth, polynomial size, unbounded fan-in
ac0_strict_nc1_ty: AC^0 ⊊ NC^1 — parity is not in AC^0 (Furst-Saxe-Sipser/Håstad)
ac_class_ty: AC (k : Nat) : Language → Prop — AC^k class (unbounded fan-in)
app
app2
app3
apsp_conjecture_ty: APSP conjecture: All-Pairs Shortest Paths requires Omega(n^3 / polylog n) time
arrow
avg_case_complete_ty: Average-case complete problem
bgs_theorem_ty: Baker-Gill-Solovay: There exist oracles A, B such that P^A = NP^A and P^B ≠ NP^B
block_sensitivity_ty: Block sensitivity of a Boolean function
bool_circuit_ty: BoolCircuit : Nat → Type — a Boolean circuit of size n
bpp_subset_bqp_ty: BPP ⊆ BQP
bqp_subset_pspace_ty: BQP ⊆ PSPACE
bs_sensitivity_relation_ty: Block sensitivity vs sensitivity: bs(f) ≤ s(f)^6 (old bound; now s(f)^2 ≥ bs(f) by Huang)
build_complexity_env: Build the computational complexity theory environment.
bvar
circuit_hierarchy_containment_ty: AC0 ⊆ TC0 ⊆ NC1
class_bpp_ty: BPP : Language → Prop — bounded-error probabilistic polynomial time
class_bqp_ty: BQP: bounded-error quantum polynomial time
class_conp_ty: coNP : Language → Prop — complement of NP
class_corp_ty: coRP : Language → Prop
class_exp_ty: EXP : Language → Prop — exponential time 2^(n^c)
class_ip_ty: IP : Language → Prop — interactive proof systems
class_l_ty: L : Language → Prop — logarithmic space
class_nexp_ty: NEXP : Language → Prop — nondeterministic exponential time
class_nl_ty: NL : Language → Prop — nondeterministic logarithmic space
class_np_ty: NP : Language → Prop — nondeterministic polynomial time
class_npspace_ty: NPSPACE : Language → Prop — nondeterministic polynomial space
class_p_ty: P : Language → Prop — polynomial time decidable
class_ph_ty: PH : Language → Prop — polynomial hierarchy
class_pp_ty: PP : Language → Prop — probabilistic polynomial time (unbounded error)
class_pspace_ty: PSPACE : Language → Prop — polynomial space
class_qcma_ty: QCMA: classical witness quantum verifier
class_qma_ty: QMA: quantum Merlin-Arthur (quantum analog of NP)
class_rp_ty: RP : Language → Prop — randomized polynomial time
class_sharp_p_ty: SharpP : Language → Prop — counting problems
class_zpp_ty: ZPP : Language → Prop — zero-error probabilistic polynomial time
clique_inapprox_ty: MaxClique is not approximable within n^(1-ε) unless P=NP
clique_monotone_lb_ty: Monotone circuit lower bound: CLIQUE requires super-polynomial monotone circuits
clique_np_complete_ty: CLIQUE is NP-complete
clique_w1_complete_ty: CLIQUE (parameterized by clique size) is W[1]-complete
comm_space_tradeoff_ty: Communication-space lower bound tradeoff
comp_indist_ty: Computational indistinguishability
cook_levin_theorem_ty: Cook-Levin theorem: SAT is NP-complete
cst
cutting_planes_ty: Cutting planes proof system
delta_p_ty: DeltaP (k : Nat) : Language → Prop
det_comm_complexity_ty: Deterministic communication complexity of a function f
determinant_ty: Determinant polynomial family
dist_np_ty: Distributional NP: NP with a distribution over inputs
distinct_elements_space_lb_ty: Distinct elements requires Omega(n) space in one-pass streaming
dspace_ty: DSPACE (f : Nat → Nat) : Language → Prop L ∈ DSPACE(f) if some TM decides L using O(f(n)) space
dtime_ty: DTIME (f : Nat → Nat) : Language → Prop L ∈ DTIME(f) if some TM decides L in O(f(n)) steps
exp_complete_ty: ExpComplete (L : Language) : Prop
fpt_algorithm_ty: FPT algorithm running in f(k) * poly(n) time
fpt_subset_xp_ty: FPT ⊆ XP (slice-wise polynomial)
fpt_ty: FPT : Language → Prop — fixed-parameter tractable
graph_property_testable_ty: Graph property testable if it has a constant query complexity tester
greedy_coloring: Greedy graph coloring (returns number of colors used and the coloring).
ham_path_np_complete_ty: HAM-PATH is NP-complete (Hamiltonian path)
hardness_amplification_ty: Hardness amplification: weak OWF → strong OWF
impagliazzo_world_ty: Impagliazzo’s worlds hypothesis (simplified: OWF exists ↔ hard on avg)
impl_pi
in_pspace_ty: PSpace: L ∈ PSPACE means L is decidable in polynomial space
information_complexity_lb_ty: Information complexity lower bound for communication
information_cost_ty: Information cost of a protocol
is_approximable_ty: IsApproximable (r : Rat) (L : Language) : Prop L has a polynomial-time r-approximation algorithm
knapsack_01: Knapsack 0/1 solver: maximize value with weight capacity. Returns (total_value, selected_item_indices).
knapsack_np_complete_ty: KNAPSACK is NP-complete
ladner_theorem_ty: Ladner’s theorem: if P ≠ NP, there exist NP-intermediate problems
language_ty: Language : Type — a set of strings (decidable predicate on strings)
levin_reduction_ty: Levin reduction (average-case reduction)
linearity_testing_ty: Linearity testing (BLR test)
local_hamiltonian_qma_complete_ty: Local Hamiltonian problem is QMA-complete
log_rank_conjecture_ty: Log-rank conjecture: D(f) ≤ poly(log rank(M_f))
logspace_reducible_ty: LogSpaceReducible (A B : Language) : Prop A ≤_m^L B — logspace many-one reduction
majority_formula_size_ty: Formula size lower bound: MAJORITY requires Omega(n^2) formula size
nat_lit
nat_ty
nc1_class_ty: NC1 circuit class: log-depth, polynomial size, fan-in 2
nc_class_ty: NC (k : Nat) : Language → Prop — NC^k class (logspace-uniform NC^k circuits)
nc_hierarchy_ty: NC hierarchy: NC^k ⊊ NC^(k+1) assuming NC ≠ P
nc_l_containment_ty: NC^1 ⊆ L ⊆ NL ⊆ NC^2 ⊆ P
nl_eq_conl_ty: Immerman-Szelepcsényi: NL = coNL
np_complete_ty: NPComplete (L : Language) : Prop — L ∈ NP ∧ NP-hard
np_hard_ty: NPHard (L : Language) : Prop — L is NP-hard under poly-many-one reductions
np_subset_pspace_ty: NP ⊆ PSPACE
nspace_ty: NSPACE (f : Nat → Nat) : Language → Prop
ntime_ty: NTIME (f : Nat → Nat) : Language → Prop L ∈ NTIME(f) if some NTM decides L in O(f(n)) steps
ntm_ty: NTM : Type — a nondeterministic Turing machine
oracle_machine_ty: OracleMachine : Language → Type — a TM with oracle access to a language
ov_conjecture_ty: OV conjecture: Orthogonal Vectors cannot be solved in O(n^(2-ε)) time
owf_exists_ty: One-way function existence
p_subset_np_ty: P ⊆ NP: every language decidable in poly-time is in NP
param_clique_w1_complete_ty: CLIQUE parameterized by k is W[1]-complete (parameterized version)
parity_not_ac0_ty: Parity not in AC0 (Håstad’s switching lemma)
pcp_theorem_ty: PCP theorem: NP = PCP(log n, 1)
permanent_ty: Permanent polynomial family
permanent_vnp_complete_ty: Valiant’s theorem: Permanent is VNP-complete
pi
pi_p_ty: PiP (k : Nat) : Language → Prop
poly_degree_ty: Polynomial degree of a Boolean function
poly_many_one_reducible_ty: PolyManyOneReducible (A B : Language) : Prop A ≤_m^p B — polynomial-time many-one reduction from A to B
poly_method_lb_ty: Polynomial method: deg(f) ≤ D(f) (approximate degree lower bounds)
poly_turing_reducible_ty: PolyTuringReducible (A B : Language) : Prop A ≤_T^p B — polynomial-time Turing reduction (Cook reduction)
polynomial_kernel_ty: Kernelization: a problem has a polynomial kernel
prg_from_owf_ty: PRG (Pseudorandom Generator) existence from OWF
prop
property_testable_ty: Testability of a boolean function property with query complexity q(ε)
pspace_complete_ty: PSPACEComplete (L : Language) : Prop
pspace_subset_exp_ty: PSPACE ⊆ EXP
qbf_pspace_complete_ty: QBF (Quantified Boolean Formula) is PSPACE-complete
quantum_comm_complexity_ty: Quantum communication complexity
quantum_pcp_conjecture_ty: Quantum PCP conjecture: QMA ⊆ MIP* = RE (negation of classical PCP analog)
rand_comm_complexity_ty: Randomized communication complexity
real_ty
resolution_proof_ty: Resolution proof system: a refutation of a CNF formula
resolution_width_ty: Width of a resolution refutation
savitch_theorem_ty: Savitch’s theorem: NPSPACE = PSPACE
sensitivity_conjecture_ty: Sensitivity conjecture (Huang 2019): s(f) ≥ sqrt(deg(f))
sensitivity_ty: Sensitivity of a Boolean function
seth_hypothesis_ty: SETH (Strong Exponential Time Hypothesis): k-SAT cannot be solved in time O(2^((1-ε)n)) for any ε > 0
seth_implies_3sum_ty: SETH implies 3SUM hardness (reduction)
shamir_theorem_ty: IP = PSPACE (Shamir’s theorem)
sigma_p_ty: SigmaP (k : Nat) : Language → Prop — k-th level of polynomial hierarchy
size_width_tradeoff_ty: Size-width tradeoff for resolution (Ben-Sasson and Wigderson)
space_hierarchy_theorem_ty: Space hierarchy theorem: DSPACE(f) ⊊ DSPACE(g) when g ≫ f
stream_space_ty: Space complexity of streaming algorithm
subset_sum: Subset sum solver: given a set of integers and a target, find a subset summing to target.
subset_sum_np_complete_ty: SUBSET-SUM is NP-complete
tc0_class_ty: TC0 circuit class: constant depth threshold circuits
tc_class_ty: TC (k : Nat) : Language → Prop — TC^k class (threshold gates)
three_coloring_np_complete_ty: 3-COLORING is NP-complete
three_sat_np_complete_ty: 3-SAT is NP-complete (reduction from SAT)
three_sum_hypothesis_ty: 3SUM hypothesis: no O(n^(2-ε)) algorithm for 3SUM on n integers
time_complexity_ty: TimeComplexity : (Nat → Nat) → Type Represents a function f : ℕ → ℕ as a time bound
time_hierarchy_theorem_ty: Time hierarchy theorem: DTIME(f) ⊊ DTIME(g) when g ≫ f ∀ f g, TimeConstructible g → (∀ n, f(n) * log(f(n)) < g(n)) → ∃ L, L ∈ DTIME(g) ∧ L ∉ DTIME(f)
tolerant_testing_ty: Tolerant property testing: distinguishes ε1-close from ε2-far
tqbf_pspace_complete_ty: TQBF is PSPACE-complete (also known as QBF)
turing_machine_ty: TuringMachine : Type — a deterministic Turing machine
type0
verify_coloring: Graph coloring checker: given a coloring, verify it uses at most k colors and no two adjacent vertices share a color.
vertex_cover_np_complete_ty: VERTEX-COVER is NP-complete
vnp_class_ty: VNP (Valiant’s NP): polynomial families in the permanent class
vp_class_ty: VP (Valiant’s P): polynomial families computed by poly-size circuits
vp_neq_vnp_conjecture_ty: VP ≠ VNP conjecture (algebraic P vs NP)
vp_subset_vnp_ty: VP ⊆ VNP
w1_ty: W[1] : Language → Prop — first level of W-hierarchy (parameterized complexity)
w_hierarchy_ty: W-hierarchy: W[1] ⊆ W[2] ⊆ … ⊆ W[P]

Module functions

Module functions Copy item path

Functions§

Module functions