絵算から等式への翻訳結果

本編「デカルト閉圏における絵算 詳細編」に対する等式的計算。

○○○ = (ba×outa);eval;inb
△△△ = Λa'[○○○]

　　　 = Λa'[(ba×outa);eval;inb]

とする。

(Λa'[(ba×outa);eval;inb]×a);[(b'a'×ina);eval;outb]

 

 = // Step1 △△△の導入と括弧の付け替え

(△△△×a);(b'a'×ina);(eval;outb)
 = // Step2 Shift（交替律）

(ba×ina);(△△△×a');(eval;outb)
 = // Step3 △△△の展開と括弧の付け替え

(ba×ina);[(Λa'[○○○]×a');eval];outb
 = // Step4 β変換

(ba×ina);[○○○];outb
 = // Step4.5 ○○○の展開

(ba×ina);[(ba×outa);eval;inb];outb
 = // Step5 交替律とid;id = id

[(ba×(ina;outa)];eval;(inb;outb)
 = // Step6 in;out = id

(ba×a);eval;b
 = // Step7 f;id = f, id;f = id

eval