Teoria typów


Teoria typów w encyklopedii

Z Wikipedii, wolnej encyklopedii Przejdź do nawigacji Przejdź do wyszukiwania

Teorią typów (ang. Type theory, niem. Typentheorie) – określa się w informatyce teoretycznej i logice matematycznej klasę systemów formalnych, w których każdy termin (ang. term, niem. Term) ma typ (ang. type, niem. 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 (ang. intuitionistic type theory, niem. intuitionistische Typentheorie).

Przypisy | edytuj kod

  1. William M. Farmer, The Seven Virtues of Simple Type Theory, Journal of Applied Logic, Vol. 6, No. 3. (September 2008), pp. 267–286.
Na podstawie artykułu: "Teoria typów" pochodzącego z Wikipedii
OryginałEdytujHistoria i autorzy