Azərbaycanca
Беларускі
Dansk
Deutsch
Española
Français
Indonesia
Italiana
日本語
Қазақ
Lietuvos
Nederlands
Português
Русский
සිංහල
แบบไทย
Türkçe
Українська
中國人
United State
Afrikaans
Інтуїціоні́стська тео́рія ти́пів (також відома як теорія Мартіна-Льофа або конструктивна теорія типів) — теорія типів, яку розробив шведський математик і філософ , опублікована в 1972 року. Метою теорії послужила формалізація конструктивної математики, конструктивні об'єкти якої, згідно з Марковим-молодшим, є «деякими фігурами, складеними з елементарних конструктивних об'єктів». У цьому напрямі логіку математики можна розглядати як частину філософії математики, у складі якої використовується.
Є кілька версій інтуїціоністської теорії типів. Сам Мартін-Льоф запропонував як [en], так і [en] варіанти теорії. На початку також представлено непредикативні версії, не сумісні з . Проте всі версії зберігають базовий стиль конструктивної логіки з використанням залежних типів.
Примітки
- Марков А. А. О конструктивной математике. Проблемы конструктивного направления в математике. 2.Конструктивный математический анализ, Сборник работ. Тр. МИАН СССР, 67, Изд-во АН СССР
- Д. Д. Рогозин; А. В. Родин. Теория типов в логике и основаниях математике. Москва, . 2016
В іншому мовному розділі є повніша стаття Intuitionistic type theory(англ.). Ви можете допомогти, розширивши поточну статтю за допомогою з англійської.
|
Вікіпедія, Українська, Україна, книга, книги, бібліотека, стаття, читати, завантажити, безкоштовно, безкоштовно завантажити, mp3, відео, mp4, 3gp, jpg, jpeg, gif, png, малюнок, музика, пісня, фільм, книга, гра, ігри, мобільний, телефон, android, ios, apple, мобільний телефон, samsung, iphone, xiomi, xiaomi, redmi, honor, oppo, nokia, sonya, mi, ПК, web, Інтернет
Intuyicioni stska teo riya ti piv takozh vidoma yak teoriya Martina Lofa abo konstruktivna teoriya tipiv teoriya tipiv yaku rozrobiv shvedskij matematik i filosof opublikovana v 1972 roku Metoyu teoriyi posluzhila formalizaciya konstruktivnoyi matematiki konstruktivni ob yekti yakoyi zgidno z Markovim molodshim ye deyakimi figurami skladenimi z elementarnih konstruktivnih ob yektiv U comu napryami logiku matematiki mozhna rozglyadati yak chastinu filosofiyi matematiki u skladi yakoyi vikoristovuyetsya Ye kilka versij intuyicionistskoyi teoriyi tipiv Sam Martin Lof zaproponuvav yak en tak i en varianti teoriyi Na pochatku takozh predstavleno nepredikativni versiyi ne sumisni z Prote vsi versiyi zberigayut bazovij stil konstruktivnoyi logiki z vikoristannyam zalezhnih tipiv PrimitkiMarkov A A O konstruktivnoj matematike Problemy konstruktivnogo napravleniya v matematike 2 Konstruktivnyj matematicheskij analiz Sbornik rabot Tr MIAN SSSR 67 Izd vo AN SSSR D D Rogozin A V Rodin Teoriya tipov v logike i osnovaniyah matematike Moskva 2016 V inshomu movnomu rozdili ye povnisha stattya Intuitionistic type theory angl Vi mozhete dopomogti rozshirivshi potochnu stattyu za dopomogoyu perekladu z anglijskoyi Divitis avtoperekladenu versiyu statti z movi anglijska Perekladach povinen rozumiti sho vidpovidalnist za kincevij vmist statti u Vikipediyi nese same avtor redaguvan Onlajn pereklad nadayetsya lishe yak korisnij instrument pereglyadu vmistu zrozumiloyu movoyu Ne vikoristovujte nevichitanij i nevidkorigovanij mashinnij pereklad u stattyah ukrayinskoyi Vikipediyi Mashinnij pereklad Google ye korisnoyu vidpravnoyu tochkoyu dlya perekladu ale perekladacham neobhidno vipravlyati pomilki ta pidtverdzhuvati tochnist perekladu a ne prosto skopiyuvati mashinnij pereklad do ukrayinskoyi Vikipediyi Ne perekladajte tekst yakij vidayetsya nedostovirnim abo neyakisnim Yaksho mozhlivo perevirte tekst za posilannyami podanimi v inshomovnij statti Dokladni rekomendaciyi div Vikipediya Pereklad