簡單輸入Lambda calculas

Question

最近開始了一個關於簡單類型lambda演算的大學模塊，對於任何剛剛（t1-> t2）或類似的例子，我從來沒有使用過這麼長的一串類型。問題是要使用類型（t1→t3）→（t2→t3→t5）→t2→t1→t7作爲短期定義的術語。我如何開始這個，我可以把它分解成更小的類型，還是必須將它作爲長類型來完成。

Answer 1

通過分開功能的類型開始。 它是一個函數，它接受4個參數並返回t7類型的東西。

• 的第一參數是被1個參數類型T1的，它返回類型T3的函數=> P1
• 的第二參數是有兩個參數的類型T2和T3的函數返回類型T5 => P2 等等

然後您需要使用這些參數和附加功能（可以說f1 ... f4）使輸入創建t7類型的東西。 當你有類型t7的東西，你將不得不把這個功能變成簡單的類型lambda微積分