有類型λ演算
維基百科,自由的 encyclopedia
有類型lambda演算是使用lambda符號()指示匿名函式抽象的一種有類型的形式化。有類型lambda演算是基礎程式語言並且是有類型的函數式程式設計語言如ML和Haskell和更間接的指令式程式語言的基礎。它們通過Curry-Howard同構密切關聯於直覺邏輯並可以被認為是範疇的類的內部語言,比如簡單類型lambda演算是笛卡爾閉範疇(CCC)的語言。
此條目沒有列出任何參考或來源。 (2017年4月5日) |
傳統上,有類型lambda演算被看作無類型lambda演算的精細化。更現代的觀點把有類型lambda演算看做更基礎的理論,而把無類型lambda演算看作它的只有一個類型的特殊情況。