Типізоване лямбда-числення

Матеріал з Вікіпедії — вільної енциклопедії.
Версія від 19:25, 22 лютого 2020, створена BunykBot (обговорення | внесок) (Категоризація)
(різн.) ← Попередня версія | Поточна версія (різн.) | Новіша версія → (різн.)
Перейти до навігації Перейти до пошуку

Типізоване лямбда-числення — це система лямбда-числення, у якій кожний вислів має тип. У цьому контексті тип — це формула певної системи числення, як-от (інтуїціоністської) пропозиційної логіки або логіки першого порядку. Типізоване Лямбда-числення з простими типами (де типи — це формули імплікаційного фрагменту інтуїціоністської логіки) має застосування на практиці в функціональних мовах програмування, як от Haskell. Складніші типізовані системи є важливими для вивчення загальних характеристик обчислюваності та у сфері автоматиції автоматичних доведень.

Посилання[ред. | ред. код]