単純にタイプされたラムダ計算式

Question

最近、単純な型指定ラムダ計算で大学のモジュールが始まりました。（t1-> t2）またはこれに類似しています。問題は、（t1→t3）→（t2→t3→t5）→t2→t1→t7のように、管理できるような短い定義を使用して用語を定義することです。どのようにすればこれを始めることができますか、それをより小さなタイプに分解することができますか、それとも長いタイプとして完成させる必要がありますか？

Answer 1

機能の種類を分けて開始してください。 4つのパラメータを取り、タイプt7のものを返す関数です。

• 第1パラメータが型T3を返すタイプT1の1つのパラメータとの関数である=> P1
• 2番目のパラメータであるタイプT5を返すタイプT2およびT3の2つのパラメータを有する関数=> P2

次に、入力をタイプt7のものにするために、これらのパラメータと追加関数（f1 ... f4と言うことがあります）を使用する必要があります。 タイプがt7のときは、この関数を単純に型指定されたラムダ計算に変更するだけです