簡單類型λ演算
維基百科,自由的 encyclopedia
簡單類型 lambda 演算()是連接詞只有
(函數類型)的有類型 lambda 演算。這使它成為規範的、在很多方面是最簡單的有類型 lambda 演算的例子。
簡單類型也被用來稱呼對簡單類型 lambda 演算的擴展比如積、陪積或自然數(系統 T)甚至完全的遞歸(如PCF)。相反的,介入了多態類型(如系統F)或依賴類型(如邏輯框架)的系統不被當作是簡單類型。簡單類型 lambda 演算最初由阿隆佐·邱奇在 1940 年介入來嘗試避免無類型 lambda 演算的悖論性使用。