Equivalence of simple rational terms is decidable

Lax149335.DecidableEquivalence · concepts/Lax149335/DecidableEquivalence.lean · lax-149335

proven

Loading review…

Natural Language Statement

Corollary

Corollary 2.8. Equivalence for simple rational terms is decidable in polynomial time.

Concept map

3 concepts

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

Each proof establishes this claim relative to its assumptions.

no assumptions

cor✓Lax149335.DecidableEquivalence

⊢Lax149335Proofs.Results.decidable_equivalence

Lean source view on GitHub

Show types on hover

1	import Lax149335.SimpleRationalTerms
2
3	/-!
4	---
5	title: Equivalence of simple rational terms is decidable
6	type: corollary
7	---
8	Corollary 2.8. Equivalence for simple rational terms is decidable in polynomial time.
9
10	# Formalization notes
11
12	Running time is not expressible here. The corollary is formalised by a decision procedure
13	that is explicit enough to make the polynomial bound evident: two simple rational terms
14	$f, g : A \to B^*$ define the same function if and only if they agree on a fixed finite set
15	$T(A)$ of test inputs, defined by induction on the type $A$ :
16
17	$\begin{aligned} T(1) &= \{()\}, & T(A_1 + A_2) &= \mathsf{Left}\, T(A_1) \cup \mathsf{Right}\, T(A_2), \\ T(A^*) &= \{[\,]\} \cup \{[a] : a \in T(A)\}, & T(A_1 \times A_2) &= T(A_1) \times \{e_2\} \;\cup\; \{e_1\} \times T(A_2), \end{aligned}$
18
19
20
21
22
23
24	where $e_i$ is a fixed element of $A_i$ (`Ty.someElem`). The number of test inputs is at
25	most the size of $A$ , every test input has size at most the size of $A$ , and a simple
26	rational term is evaluated on an input in polynomial time.
27	-/
28
29	namespace Lax149335.DecidableEquivalence
30
31	open Lax149335.Types Lax149335.SimpleRationalTerms
32
33	/-- The test inputs `T(A)` of a type. -/
34	def testInputs : (A : Ty) → List ⟦A⟧
35	\| .unit => [()]
36	\| .sum A₁ A₂ => (testInputs A₁).map Sum.inl ++ (testInputs A₂).map Sum.inr
37	\| .prod A₁ A₂ =>
38	(testInputs A₁).map (fun a => (a, Ty.someElem A₂)) ++
39	(testInputs A₂).map (fun b => (Ty.someElem A₁, b))
40	\| .list A => [] :: (testInputs A).map (fun a => [a])
41
42	/-- Corollary 2.8. Two simple rational terms define the same function if and only if they
43	agree on all test inputs. -/
44	axiom decidable_equivalence {Bs : Type} {A : Ty} (f g : SimpleTerm Bs A) :
45	f.den = g.den ↔ ∀ x ∈ testInputs A, f.den x = g.den x
46
47	end Lax149335.DecidableEquivalence
48

Show Proof

Formalization notes

Running time is not expressible here. The corollary is formalised by a decision procedure that is explicit enough to make the polynomial bound evident: two simple rational terms $f, g : A \to B^*$ define the same function if and only if they agree on a fixed finite set $T(A)$ of test inputs, defined by induction on the type $A$ :

\begin{aligned} T(1) &= \{()\}, & T(A_1 + A_2) &= \mathsf{Left}\, T(A_1) \cup \mathsf{Right}\, T(A_2), \\ T(A^*) &= \{[\,]\} \cup \{[a] : a \in T(A)\}, & T(A_1 \times A_2) &= T(A_1) \times \{e_2\} \;\cup\; \{e_1\} \times T(A_2), \end{aligned}

where $e_i$ is a fixed element of $A_i$ ( $Ty.someElem$ ). The number of test inputs is at most the size of $A$ , every test input has size at most the size of $A$ , and a simple rational term is evaluated on an input in polynomial time.

Builds on

Lax149335.SimpleRationalTerms

Used by

none

From Mathlib

none

Discussion

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

Loading discussion…

Lax Lean Archive

Equivalence of simple rational terms is decidable

Flags

Flag this concept

Natural Language Statement

Corollary

Lean source view on GitHub

Discussion

Settings

Your comments