full abstraction ... λ計算とかπ計算とか表示的意味論のお話ではよく出てくる概念なんですが、未だによくわからないなーとつぶやいていたら id:sumii さんに教えていただいた。 もったいないのでここに残しておきます。 full abstraction の私的な説明 計算…

sumiiさんの記事によれば，どうも私は [お勉強]とタグをつけたのをいいことにデマを振りまいていたようなので訂正しました．型付きλ計算の型でcharacterizeしてるから論理的，というのなら，正直 Curry-Howard同型による，という説明でもそれほど間違ってな…

ATTAPL続き． 論理関係とは 論理関係は λ計算の項の間の2項関係で, 型でインデックスがついている(つまり型を含めれば3項関係). 論理関係は「論理的」な関係である(Curry-Howard的な意味で). すなわち，論理関係とは R(s1, t1, T1->T2) かつ R(s2, t2, T1) …

ATTAPLの6章は 論理関係という方法を使ったプログラムの等価性検査について書いてある．6.3節では, 前準備として, 基本型がプログラムの等価性に影響を与える場合について述べている．ここではλ計算にUnit型を入れてプログラムの等価性を議論している. Unit…