Comment by JonChesterfield
2 years ago
Equality works out cleanly if you distinguish between definitional equality and equivalence. Definitional sometimes gets called syntactic. As in the definitions are the same symbols in the same arrangement.
(lambda (x) (+ x x)) != (lambda (x) (* 2 x))
In particular, that's decidable on any finite expressions. Walk the expressions like an AST comparing the nodes on each side.
Equivalence / observational equality covers whether two expressions compute the same thing. As in find a counterexample to show they're not equivalent, or find a proof that both compute the same things, or that each can be losslessly translated into the other.
Requiring that your language can decide observational equivalence on the computation of any two terms seems obviously a non-starter to me, but it also looks like the same thing as requiring a programming language type system be decidable.
I want to reason hypothetically, which is why I don't use syntactic equality. I only use syntactic inequality in a very limited sense, e.g. two symbols `foo'` and `bar'` are symbolic distinct, so one can introduce `sd(foo', bar')`.
The reason is that if I have a proof `((x + x) == (2 * x))^true`, then I can treat objects as if they were definitionally equal.
When definitional equality and syntactic equality are the same, one is assuming `(!(sd(a, b)) == (a == b))^true`, which obtains a proof `!sd(a, a)` for all `a`. This destroys the property of reasoning hypothetically about exponential propositions in Path Semantics. For example, I might want to reason about what if I had `sd(a, a)`, does this imply `a ~~ a` by `q_lift : sd(a, b) & (a == b) -> (a ~~ b)`? Yes!
However, if I already have `!sd(a, a)` for all `a`, then the above reasoning would be the same absurd reasoning.
I can always assume this in order to reason about it, but I don't have to make this assumption a built-in axiom of my theory.
When assuming tautological congruence e.g. `(a == b)^true` in a context, one is not enforcing observational equality. So, it is not the same as requiring the type system to be decidable. I can also make up new notions of equivalences and guard them, e.g. not making them tautological congruent.
I don't follow. At a guess, my "definitional equality" is your "syntactic equality", but I can't infer what you mean by definitional. Perhaps our terminology is too different to communicate successfully.
(+ X X) is not definitionally equal to (* 2 X), for they are different definitions. Different pictures on the page. A proof that they are equivalent is not a proof that they are equal. A proof that they are equal is evidence that your proof system is unsound.
If you assume a symbol is not definitionally equal to itself, you can indeed prove false, but that doesn't seem particularly important since you cannot prove that a symbol has a different definition to itself.
Yeah, this is too imprecise. I tried to translate to your terminology, but failed.
My system uses "tautological equality" and this allows me to treat them the save way for all tautological congruent operators. Ofc, you can't treat them the same if an operator is neither normal nor tautological congruent.
Even if you have a such operator `foo'(x)` you can prove `foo'(x)`, `(foo'(x) == foo'(x))^true` or `foo'(x) == foo'(x)` etc. If this is what you are talking about, then this system supports it.