Топ питань
Часова шкала
Чат
Перспективи

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

З Вікіпедії, вільної енциклопедії

Remove ads

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

Remove ads

Див. також

Посилання

Loading related searches...

Wikiwand - on

Seamless Wikipedia browsing. On steroids.

Remove ads