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

日々の流転


2009-03-04 [長年日記]

λ. IDPで数独を解く

数独をParadoxDarwinMaceで解いてみたので、ついでにIDPでも試してみた*1

IDPの特徴は帰納的定義が出来ることのようだ(普通の一階述語論理では帰納的な定義は出来ない)。 具体的には { R(t1,…,tn) <- 論理式. } 等と書けて、論理式の中でRを使うことで、関係Rを帰納的に定義出来る。 帰納的定義が出来るということは、例えば推移閉包を公理化出来るので、グラフが関係してくるようなパズルを解くのには向いていそうだ。

あと、記述言語では例によって、感嘆符「!」と疑問符「?」がそれぞれ全称量化子と存在量化子として用いられている。

*1 同じネタをひっぱり過ぎ