2008-04-03 [長年日記]
λ. 確定記述(definite description)
『圏論による論理学—高階論理とトポス』 に確定記述 ιx(φx) というものが出てきた。 「これは φx を満たす唯一つの x」を表す式で、一階述語論理での解釈はこんな感じになる。
ψ(ιx(φx)) := ∃x(∀y(φy ↔ y = x) ∧ ψx)
「これは部分継続を使って解釈できるじゃん♪」とか一瞬喜んだが、考えてみれば一般化量化子(generalized quantifier)なわけで、解釈できて当たり前だった。 しかも、そういえば hsPTQにも確定記述の the を一般化量化子として実装していたわけで、何をぼけているんだ、私。
関連
[ツッコミを入れる]
