Matematik ve bilgisayar bilimlerinde, tip teorisi belirli bir tip sistemin resmi sunumudur. Tip teorisi genel olarak tip sistemlerinin akademik çalışmasıdır.
Bazı tip teoriler, matematiğin küme teorisine alternatif olarak hizmet
eder. Temel olarak önerilen iki etkili tip teorisi, Alonzo Church’nün tip λ-kalkülüs’ü
ve Per Martin-Löf'ün sezgisel tip teorisidir.
Çoğu bilgisayarlı kanıt yazma sistemi, temelleri için bir tip teorisi
kullanır. Yaygın olanı biri, Thierry Coquand'ın Endüktif Yapılar Hesabı’dır.
Martin-Löf bağımlı tip teorisi; tablo, bağımlı tip teorisinin
kavramlarının karşılık gelen kategorik anlamlarını gösterir (dependent
type theory)
Alonzo Church’nün 0, 1, 2, ..., için llambda tanımları (Church encoding)
https://en.wikipedia.org/wiki/Type_theory
12 Aralık 2023
GERİ (matematik anasayfa)
