| dbo:abstract
|
- La teoria de tipus intuicionista, en anglès: Intuitionistic type theory (també coneguda com a constructive type theory, o Martin-Löf type theory) és una i un alternatiu basada en els principis del . Aquesta teoria va ser presentada pel matemàtic suec 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 . Formulacoons posteriors si eren predicatives. La eoria de tipus intuicionista està basada en certes analogies o isomorfismes entre proposicions i tipus. Aquesta teoria internalitza la interpretació de la proposada per Brouwer, Heyting i Kolmogórov, l'anomenada com . (ca)
- Intuitionistic type theory (also known as constructive type theory, or Martin-Löf type theory) is a type theory and an alternative foundation of mathematics.Intuitionistic type theory was created by Per Martin-Löf, a Swedish mathematician and philosopher, who first published it in 1972. There are multiple versions of the type theory: Martin-Löf proposed both intensional and extensional variants of the theory and early impredicative versions, shown to be inconsistent by Girard's paradox, gave way to predicative versions. However, all versions keep the core design of constructive logic using dependent types. (en)
- 直観主義型理論（ちょっかんしゅぎかたりろん、英: intuitionistic type theory）とは、数学の代替基盤を目指して論理学・哲学者のペール・マルティン＝レーフによって開発された型理論を言う。構成的型理論（constructive type theory）、またはマルティン＝レーフの型理論（Martin-Löf's type theory）とも呼ばれる。1972年に最初のバージョンが発表された。直観主義型理論には複数のバージョンがある。 マルティン＝レーフは当初非可述的な定義が可能な型理論を構築していたが、ジャン＝イヴ・ジラール（Jean-Yves Girard）によってパラドックスを起こすことが指摘され一時頓挫した（）。その後、パラドックスを起こさない可述的なバージョンが発表された。ただし、すべてのバージョンは、依存型を使用した構成的論理のコア設計を維持している。 (ja)
- La teoria dei tipi intuizionista (nota anche come teoria dei tipi costruttiva o teoria dei tipi di Martin-Löf) è una teoria dei tipi e una fondazione della matematica alternativa. Fu creata da , matematico e filosofo svedese, che la pubblicò per la prima volta nel 1972. Esistono diverse versioni della teoria: Martin-Löf ha proposto varianti , e inizialmente , delle quali ha mostrato l'incoerenza, dando il via alle versioni . Tuttavia, tutte le versioni mantengono il design centrale della logica costruttiva, utilizzando tipi dipendenti. (it)
- Teoria dos tipos intuicionista, ou Teoria dos tipos construtiva, ou Teoria dos tipos de Martin-Löf é uma teoria dos tipos e uma alternativa para os fundamentos da matemática baseados nos princípios do construtivismo matemático. A teoria de tipos intuicionista foi introduzida por Per Martin-Löf, um matemático e filósofo sueco, em 1972. Martin-Löf modificou sua proposta algumas vezes; sua formulação impredicativa de 1971 era inconsistente, como demonstrado pelo paradoxo de Girard. As próximas formulações eram predicativas. Ele propôs tanto uma variante intensional quanto uma variante extensional da teoria. A teoria dos tipos intuicionista é baseada em uma certa lógica ou isomorfismo entre proposições e tipos: uma proposição é identificada com o tipo de suas provas. Essa identificação é usualmente chamada de isomorfismo de Curry-Howard, que originalmente foi formulado para a lógica intuicionista e para o cálculo lambda simplesmente tipado. A Teoria dos Tipos estende sua identificação para a lógica de predicados através da introdução de tipos dependentes, que são tipos que contêm valores. A Teoria dos Tipos internaliza a interpretação da lógica intuicionista proposta por Brouwer, Heyting e Kolmogorov, também chamada de interpretação BHK. Os tipos da Teoria dos Tipos possuem um papel similar aos conjuntos da teoria dos conjuntos, mas as funções definidas na Teoria dos Tipos são sempre computáveis. (pt)
- Интуиционистская теория типов (также известна, как теория Мартина-Лёфа или конструктивная теория типов) — теория типов, разработанная шведским математиком и философом Пером Мартином-Лёфом, была опубликована в 1972 году. Целью теории послужила формализация конструктивной математики, конструктивные объекты которой, согласно Маркову-младшему, являются «некоторыми фигурами, составленными из элементарных конструктивных объектов». В данном направлении логика математики может рассматриваться как часть философии математики, в составе которой и используется. Имеются несколько версий интуиционистской теории типов. Самим Мартином-Лёфом предложены как , так и варианты теории. В начале были также представлены непредикативные версии, не совместимые с . Тем не менее, все версии сохраняют базовый стиль конструктивной логики с использованием зависимых типов. (ru)
- 直觉类型论（英語：Intuitionistic type theory），也可简称类型论，此外也有构造类型论或马汀-洛夫类型论称呼。是基于数学构造主义的函数式编程语言、逻辑和集合论。 直觉类型论由瑞典数学家和哲学家 佩尔·马丁-洛夫于1972年引入。此前马丁已经多次修改了他的提议，先是非直谓性的而后是直谓性的，先是外延的而后是内涵的类型论变体。直觉类型论基于的是命题和等价类的同一一个命题同一于它的证明的类型。这种同一通常叫做柯里-霍华德同构，它最初公式化了命题逻辑和简单类型λ演算。 类型论通过介入包含着值的依赖类型把这种同一扩展到谓词逻辑。类型论内在化了 鲁伊兹·布劳威尔、阿兰德·海廷 和 安德雷·柯爾莫哥洛夫提议的布劳威尔-海廷-柯尔莫哥洛夫释义的直觉逻辑释义。类型论的类型扮演了类似于集合在集合论的角色，但是在类型论中的函数总是可计算的。 (zh)
|
| rdfs:comment
|
- Intuitionistic type theory (also known as constructive type theory, or Martin-Löf type theory) is a type theory and an alternative foundation of mathematics.Intuitionistic type theory was created by Per Martin-Löf, a Swedish mathematician and philosopher, who first published it in 1972. There are multiple versions of the type theory: Martin-Löf proposed both intensional and extensional variants of the theory and early impredicative versions, shown to be inconsistent by Girard's paradox, gave way to predicative versions. However, all versions keep the core design of constructive logic using dependent types. (en)
- 直観主義型理論（ちょっかんしゅぎかたりろん、英: intuitionistic type theory）とは、数学の代替基盤を目指して論理学・哲学者のペール・マルティン＝レーフによって開発された型理論を言う。構成的型理論（constructive type theory）、またはマルティン＝レーフの型理論（Martin-Löf's type theory）とも呼ばれる。1972年に最初のバージョンが発表された。直観主義型理論には複数のバージョンがある。 マルティン＝レーフは当初非可述的な定義が可能な型理論を構築していたが、ジャン＝イヴ・ジラール（Jean-Yves Girard）によってパラドックスを起こすことが指摘され一時頓挫した（）。その後、パラドックスを起こさない可述的なバージョンが発表された。ただし、すべてのバージョンは、依存型を使用した構成的論理のコア設計を維持している。 (ja)
- La teoria dei tipi intuizionista (nota anche come teoria dei tipi costruttiva o teoria dei tipi di Martin-Löf) è una teoria dei tipi e una fondazione della matematica alternativa. Fu creata da , matematico e filosofo svedese, che la pubblicò per la prima volta nel 1972. Esistono diverse versioni della teoria: Martin-Löf ha proposto varianti , e inizialmente , delle quali ha mostrato l'incoerenza, dando il via alle versioni . Tuttavia, tutte le versioni mantengono il design centrale della logica costruttiva, utilizzando tipi dipendenti. (it)
- 直觉类型论（英語：Intuitionistic type theory），也可简称类型论，此外也有构造类型论或马汀-洛夫类型论称呼。是基于数学构造主义的函数式编程语言、逻辑和集合论。 直觉类型论由瑞典数学家和哲学家 佩尔·马丁-洛夫于1972年引入。此前马丁已经多次修改了他的提议，先是非直谓性的而后是直谓性的，先是外延的而后是内涵的类型论变体。直觉类型论基于的是命题和等价类的同一一个命题同一于它的证明的类型。这种同一通常叫做柯里-霍华德同构，它最初公式化了命题逻辑和简单类型λ演算。 类型论通过介入包含着值的依赖类型把这种同一扩展到谓词逻辑。类型论内在化了 鲁伊兹·布劳威尔、阿兰德·海廷 和 安德雷·柯爾莫哥洛夫提议的布劳威尔-海廷-柯尔莫哥洛夫释义的直觉逻辑释义。类型论的类型扮演了类似于集合在集合论的角色，但是在类型论中的函数总是可计算的。 (zh)
- La teoria de tipus intuicionista, en anglès: Intuitionistic type theory (també coneguda com a constructive type theory, o Martin-Löf type theory) és una i un alternatiu basada en els principis del . Aquesta teoria va ser presentada pel matemàtic suec 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 . Formulacoons posteriors si eren predicatives. La eoria de tipus intuicionista està basada en certes analogies o isomorfismes entre proposicions i tipus. (ca)
- Teoria dos tipos intuicionista, ou Teoria dos tipos construtiva, ou Teoria dos tipos de Martin-Löf é uma teoria dos tipos e uma alternativa para os fundamentos da matemática baseados nos princípios do construtivismo matemático. A teoria de tipos intuicionista foi introduzida por Per Martin-Löf, um matemático e filósofo sueco, em 1972. Martin-Löf modificou sua proposta algumas vezes; sua formulação impredicativa de 1971 era inconsistente, como demonstrado pelo paradoxo de Girard. As próximas formulações eram predicativas. Ele propôs tanto uma variante intensional quanto uma variante extensional da teoria. (pt)
- Интуиционистская теория типов (также известна, как теория Мартина-Лёфа или конструктивная теория типов) — теория типов, разработанная шведским математиком и философом Пером Мартином-Лёфом, была опубликована в 1972 году. Целью теории послужила формализация конструктивной математики, конструктивные объекты которой, согласно Маркову-младшему, являются «некоторыми фигурами, составленными из элементарных конструктивных объектов». В данном направлении логика математики может рассматриваться как часть философии математики, в составе которой и используется. (ru)
|
