7
$\begingroup$

I want to know why we add an intensional equality in type theory to definitional equality ? What is the aim with this intensional equality ?

thanks

$\endgroup$
4
  • 1
    $\begingroup$ Intensional equality is decidable but extensional equality is not. I guess mathematics is not intensional since I can't decide whether or not that was the reason... $\endgroup$ Aug 3, 2012 at 1:32
  • $\begingroup$ Not all type theories use intentional equality. For example, Martin-Lof has developed type theories with intentional and with extensional equality. Each one has its own cons and pros. $\endgroup$
    – Kaveh
    Aug 3, 2012 at 5:20
  • 1
    $\begingroup$ Do you mean to ask about intensional versus extensional equality, or propositional versus definitional/judgmental equality? Propositional equality can be either intensional or extensional (e.g. depending on whether or not it satisfies axiom K). $\endgroup$ Aug 3, 2012 at 5:28
  • 1
    $\begingroup$ Try looking at Chapter 8 of B. Nordström, et al., Programming in Martin-Löf’s Type Theory, intuitionistic.files.wordpress.com/2010/07/… $\endgroup$ Sep 3, 2012 at 11:33

1 Answer 1

7
$\begingroup$

The key thing to notice is that the definitional equality is a judgement and not a proposition (so in particular, definitional equalities can not be part of your assumptions, nor can they be proved, they can only be checked by the type-checker). The intensional equality, on the other hand, is a proposition, so it can be used as an assumption, and we can e.g. use induction to prove an intensional equality.

The two equalities are closely connected, but do not generally agree: Martin-Löf's intensional type theory has decidable type checking, and hence also the definitional equality judgement is decidable, but you can convince yourself that the intensional equality is not decidable.

Note that definitional equality entails intensional equality, but not the other way around.

$\endgroup$
2
  • $\begingroup$ As a clarification, the first paragraph here would also apply to an extensional, propositional equality. $\endgroup$ Sep 3, 2012 at 5:51
  • $\begingroup$ I believe kow is saying that one can use structural induction to prove an intensional equality, because there are rules to allow this, but there are not rules to manipulate definitional equality. $\endgroup$ Sep 3, 2012 at 11:29

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.