Teoria typów

Teoria typów – klasa systemów formalnych w informatyce teoretycznej i logice matematycznej, w których każdy termin ma typ, a operacje są ograniczone do terminów określonego typu^[1]. Teoria typów może służyć jako alternatywa dla teorii zbiorów jako podstawy dla całej matematyki. Teoria typów jest ściśle związana z systemami typów (i częściowo pokrywa się z nimi), które są funkcją języków programowania zmniejszającą liczby błędów. Dwie najbardziej znane teorie typów to typ rachunku λ Alonzo Churcha i intuicyjna teoria typów Per Martina-Löfa.

Przypisy[edytuj | edytuj kod]

↑ William M. Farmer, The Seven Virtues of Simple Type Theory, Journal of Applied Logic, Vol. 6, No. 3. (September 2008), pp. 267–286.

Theory of types (ang.), Routledge Encyclopedia of Philosophy, rep.routledge.com [dostęp 2023-05-10].

logika matematyczna	algebraiczna mereologia rachunek zdań teoria dowodu teoria modeli teoria rekursji teoria typów
metamatematyka	metalogika
teoria mnogości	opisowa arytmetyka liczb kardynalnych arytmetyka liczb porządkowych teoria PCF
teoria obliczeń	teoria obliczalności teoria złożoności
inne	teoria kategorii filozofia matematyki