Siirry offline-tilaan Player FM avulla!
Extensional Martin-Loef Type Theory
Manage episode 354442676 series 2823367
In this episode, I discuss the basic distinguishing rule of Extensional Martin-Loef Type Theory, namely equality reflection. This rule says that propositional equality implies definitional equality. Algorithmically, it would imply that the type checker should do arbitrary proof search during type checking, to see if two expressions are definitionally equal. This immediately gives us undecidability of type checking for the theory, at least as usually realized.
166 jaksoa
Manage episode 354442676 series 2823367
In this episode, I discuss the basic distinguishing rule of Extensional Martin-Loef Type Theory, namely equality reflection. This rule says that propositional equality implies definitional equality. Algorithmically, it would imply that the type checker should do arbitrary proof search during type checking, to see if two expressions are definitionally equal. This immediately gives us undecidability of type checking for the theory, at least as usually realized.
166 jaksoa
Kaikki jaksot
×Tervetuloa Player FM:n!
Player FM skannaa verkkoa löytääkseen korkealaatuisia podcasteja, joista voit nauttia juuri nyt. Se on paras podcast-sovellus ja toimii Androidilla, iPhonela, ja verkossa. Rekisteröidy sykronoidaksesi tilaukset laitteiden välillä.