トップ «前の日記(2008-04-02) 最新 次の日記(2008-04-04)» 月表示 編集

日々の流転


2008-04-03 [長年日記]

λ. 確定記述(definite description)

『圏論による論理学—高階論理とトポス』 に確定記述 ιx(φx) というものが出てきた。 「これは φx を満たす唯一つの x」を表す式で、一階述語論理での解釈はこんな感じになる。

ψ(ιx(φx)) := ∃x(∀y(φy ↔ y = x) ∧ ψx)

「これは部分継続を使って解釈できるじゃん♪」とか一瞬喜んだが、考えてみれば一般化量化子(generalized quantifier)なわけで、解釈できて当たり前だった。 しかも、そういえば hsPTQにも確定記述の the を一般化量化子として実装していたわけで、何をぼけているんだ、私。

関連