Топ питань
Часова шкала
Чат
Перспективи
Типізоване лямбда-числення
З Вікіпедії, вільної енциклопедії
Remove ads
Типізоване лямбда-числення — це система лямбда-числення, у якій кожний вислів має тип. У цьому контексті тип — це формула певної системи числення, як-от (інтуїціоністської) пропозиційної логіки або логіки першого порядку. Типізоване Лямбда-числення з простими типами (де типи — це формули імплікаційного фрагменту інтуїціоністської логіки) має застосування на практиці в функціональних мовах програмування, як от Haskell. Складніші типізовані системи є важливими для вивчення загальних характеристик обчислюваності та у сфері автоматиції автоматичних доведень.
Remove ads
Див. також
Посилання
Ця стаття не містить посилань на джерела. (грудень 2015) |
![]() |
![]() |
Це незавершена стаття про інформаційні технології. Ви можете допомогти проєкту, виправивши або дописавши її. |
Wikiwand - on
Seamless Wikipedia browsing. On steroids.
Remove ads