Decidability of propositional equaility

2
votes

Two terms in agda are said to be definitionally equal precisely when they both have the same normal form ---I think---, and propositional equality is just the data-type representation of definitional equality ---again, I guess---; so then shouldn't propositionally equality be decidable? That is, would it seem reasonable that we can write a function typed

∀{A : Set} → (x y : A) → Dec(x ≡ y).

I kinda of get that we cannot write such a function since we cannot pattern match on the arguments, but I 'feel' that it should be possible: again, just reduce to normal form and check for syntactic identity.

Any insight would be helpful!

1
equalityagdadependent-type

1 Answers

3
votes

Two terms in agda are said to be definitionally equal precisely when they both have the same normal form

Up to αη-conversion.

and propositional equality is just the data-type representation of definitional equality

Propositional equality says "these two terms will become definitionally equal after you instantiate some free variables" ("some" can be 0 or all of them) ("instantiate" can vary too).

E.g.

double-double : (n : ℕ) -> n + n ≡ 2 * n

clearly, n + n is not syntactically equal to 2 * n, but for any canonical n (0, 1, 2...) the result of n + n is syntactically equal to the result of 2 * n — that's what double-double says. And that "for any canonical n" part forces us to prove double-double by induction (though, in a more complicated system, where definitional equality is based on supercompilation or there is a build-in prover, n + n is definitionally equal to 2 * n).

But sometimes it's not as obvious how an induction hypothesis should look like, e.g. when you need to generalize an equation. As you might expect, there is no decision procedure for "is this arbitrary thing provable?" and hence propositional equality is undecidable. Moreover, you can't neither prove nor disprove statements like

(λ n -> 1 + n) ≡ (λ n -> n + 1)

without additional postulates.

However you really can check for syntactic equality:

_≟_ : ∀ {α} {A : Set α} -> (x y : A) -> Maybe (x ≡ y)

It says "if two terms are syntactically equal, then they are equal propositionally, otherwise we don't know whether they are equal propositionally or not". But Agda doesn't have such built-in function.