構造演算維基百科,自由的 encyclopedia 構造演算(CoC)是高階有類型 lambda 演算,這裡的類型是一級值。因此在 CoC 內有可能定義從整數到類型、從類型到類型的函數,同從整數到整數的函數一樣。CoC 是強規範化的。 CoC 最初由 Thierry Coquand 開發。 CoC 是 Coq 定理證明器早期版本的基礎;它後來的版本建造在歸納構造演算之上,這是帶有對歸納數據類型的天然支持的 CoC 擴展。在最初的 CoC 中,歸納數據類型必須模擬為它們的多態解構函數。
構造演算(CoC)是高階有類型 lambda 演算,這裡的類型是一級值。因此在 CoC 內有可能定義從整數到類型、從類型到類型的函數,同從整數到整數的函數一樣。CoC 是強規範化的。 CoC 最初由 Thierry Coquand 開發。 CoC 是 Coq 定理證明器早期版本的基礎;它後來的版本建造在歸納構造演算之上,這是帶有對歸納數據類型的天然支持的 CoC 擴展。在最初的 CoC 中,歸納數據類型必須模擬為它們的多態解構函數。