La teoria de tipus intuïcionista, en anglès: Intuitionistic type theory (també coneguda com a constructive type theory, o Martin-Löf type theory) és una teoria de tipus i un fonament matemàtic alternatiu basada en els principis del constructivisme matemàtic. Aquesta teoria va ser presentada pel matemàtic suec Per Martin-Löf el 1972. Martin-Löf l'ha modificada unes poques vegades, la seva formulació impredicativa de l'any 1971 era inconsistent com va demostrar la Paradoxa de Girard. Formulacions posteriors si eren predicatives.
La teoria de tipus intuïcionista està basada en certes analogies o isomorfismes entre proposicions i tipus.
Aquesta teoria internalitza la interpretació de la lògica intuicionista proposada per Brouwer, Heyting i Kolmogórov, l'anomenada com BHK interpretation.
Bibliografia
- Bengt Nordström; Kent Petersson; Jan M. Smith (1990). Programming in Martin-Löf's Type Theory. Oxford University Press. The book is out of print, but a free version can be picked up from here.
- Thompson, Simon (1991). Type Theory and Functional Programming Addison-Wesley. ISBN 0-201-41667-0.
- Granström, Johan G. (2011). Treatise on Intuitionistic Type Theory Springer. ISBN 978-94-007-1735-0.
Enllaços externs
- EU Types Project: Tutorials - lecture notes and slides from the Types Summer School 2005
- n-Categories - Sketch of a Definition - letter from John Baez and James Dolan to Ross Street, November 29, 1995
Wikiwand in your browser!
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.
