プログラムの等価性と型

お勉強

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

   Γ |- s:Unit     Γ |- t:Unit
------------------------------------ [Q-UNIT]
      Γ |- s ≡ t : Unit

いっぽう，これより弱い規則を考えることもできる．他の基本型と同様に，syntacticな等価性のみを使う：

------------------------------------ [Q-UNIT-WEAK]
      Γ |- unit ≡ unit : Unit

が この規則では 等価であるはずの x:Unit, y:Unit |- x ≡ y : Unit を導出できない．

Exercise 6.3.1

Q. 上の x や y は変数を含む open な項だが， closed な項についても (Q-UNIT のような) 型に固有の等価性の規則が必要となる． 別々の正規形を持つが等価である項を答えよ．

A. λx:Unit.x と λx:Unit.unit

これらの項の等価性を示すには Q-UNIT を使うしかない．

-------------------- [T-VAR]   ------------------------ [T-UNIT]
  x:Unit |- x:Unit                x:Unit |- unit:Unit
------------------------------------------------------------ [Q-UNIT]
                 x:Unit |- x ≡ unit : Unit
     --------------------------------------------------- [Q-ABS]
       |- λx:Unit.x ≡ λx:Unit.unit : Unit → Unit

木の根から2段目でQ-UNITが必要になる． Q-ABS の代わりに Q-EXTを使って Q-BETA を使って簡約してもほぼこの形に落ちる．

雑感

とりあえず論理関係まではわかりたいと思って読んでいます