日々の流転

λ. uniform proof

論理プログラミングの世界に uniform proof という概念があることを偶然知った。<URL:http://www.lix.polytechnique.fr/Labo/Dale.Miller/lolli/> の説明が分かりやすかったので以下に引用。

In order to determine whether a logic more expressive than Horn clauses (the logic of Prolog) could still be seen as the foundation of a logic programming language, Miller and Nadathur carefully analyzed the notion of goal-directedness and made the following definition. A proof is goal directed (or, in their words, uniform) if whenever a sequent has a non-atomic formula as its right hand side (that is, as the goal) then the rule used at that point is the one to decompose the goal. Logic programming, as distinct from theorem proving, can be seen as the search for uniform proofs. A logic is appropriate as a foundation of a logic programming language if uniform proofs are complete for that logic.

λ. 北朝鮮の核実験

あー、やるだろうとは思ってたけどついにやっちゃったのね。

結局、太陽政策を初めとする宥和政策は先送りに過ぎず、その間に脅威が単に増しただけだったのでしょうか?

(後でもう少し書く)