Unfortunately, because propositional equality is undecidable, equality reflection ensures that it is undecidable whether a judgment of the theory holds; worse, as hinted previously, even the “definitional fragment” of the resulting judgmental equality can no longer be automated, because β-reduction of open terms may diverge. If, on the other hand, one omits β-equivalence from judgmental equality, it is possible to retain decidability of judgments in a dependently-typed language with divergent terms, as in the Zombie language.

Huh. Not really sure what beta equivalence is referring to but it seems odd to... not consider reducing functions when checking equivalence

Sign in to participate in the conversation

A Mastodon instance for users who like the study of programming languages, formal semantics, types, or linguistics.