日々の流転

λ. 「掛け算から足し算を作る」を定理証明器で

檜山さんの「掛け算から足し算を作る（パズルとしてやってみよう）」の証明の部分を定理証明器に証明させてみようとしてみた……がうまくいかず。

SPASS で試してみたのが AGS.dfg で、The E Equational Theorem Prover(eprover) で試してみたのが AGS.tptp 。 どちらの場合でも、conjectureを一個ずつ試したところ、x+0=x と加算に関する逆元の存在はすぐに証明できるのだけど、他は組み合わせ爆発している感じ。 適当に補題を追加すればいいかと思ったけど、それでもそもそも公理の数が多いとダメみたい。 ……残念無念。

λ. CLTT の 1.1 Fibrations の練習問題

CLTT読書会で読んでいる、Categorical Logic and Type Theory だけど、最近全然ちゃんと読めていなかったので、一念発起して復習することに。まずは、1.1 Fibrations の練習問題を解いてみた(解いた時のメモ)。 このメモは Note Taker HD で書いてみた(参考: iPadを紙代わりに使うならNote Taker HD - a geek born in Tomakomai)。

λ. IDPで 3 not problem を解けなかった

以前に

• 3 not problem - ヒビルテ(2008-07-16)
• Alloy で 3 not problem を解く - ヒビルテ(2008-07-16)
• Otter で 3 not problem を解く - ヒビルテ(2008-07-18)

辺りで書いた 3 not problem (別名: The 2-inverter puzzle) を、IDP (Inductive Definition Programming) で解いてみようとした。 が、うまくいかなかったという話。

回路の構成自体を解として直接求めるのは、Alloyや他のソルバーでうまくいってなかったので、Otterの場合と同じく、notを使う箇所だけを解として求めることにした。 具体的には「notを適用する真理値表Inv1,Inv2が与えられた時に真理値表xsが計算可能である」ことを表す述語P(xs)を帰納的に定義して、出力となる真理値表がこの述語を満たすときのInv1,Inv2の値を解として求める。 一階述語論理の普通のモデル発見器では帰納的な定義ができないので、こういうやり方を出来るのは、IDPとかASPくらいのはず。

定式化自体は two_inv.idp.gz のように非常に簡単にできた。ただ、ビット演算のやり方が分からないので、そこは定数とテーブルを自前で用意することで対処した。その辺りのつまらない部分を省略したものを以下に示す。

Given:
  type BV8 = {
B00000000;
B00000001;
〜(中略)〜
B11111111;
} 
  BIT_NOT (BV8) : BV8
  BIT_AND (BV8,BV8) : BV8
  BIT_OR (BV8,BV8) : BV8

Find:
  Inv1 : BV8
  Inv2 : BV8

Declare:
  P (BV8)

Satisfying:
  { P(B00001111). // input 1
    P(B00110011). // input 2
    P(B01010101). // input 3
    P(BIT_AND(x,y))  <- P(x) & P(y).
    P(BIT_OR(x,y))   <- P(x) & P(y).
    P(BIT_NOT(Inv1)) <- P(Inv1).
    P(BIT_NOT(Inv2)) <- P(Inv2).
  }
  P(B11110000). // output 1
  P(B11001100). // output 2
  P(B10101010). // output 3

Data:
  BIT_NOT = { 
B00000000 -> B11111111;
〜(中略)〜
B11111111 -> B00000000;
}

  BIT_AND = {
B00000000,B00000000 -> B00000000;
B00000000,B00000001 -> B00000000;
〜(中略)〜
B11111111,B11111111 -> B11111111;
}

  BIT_OR = {
B00000000,B00000000 -> B00000000;
B00000000,B00000001 -> B00000001;
〜(中略)〜
B11111111,B11111111 -> B11111111;
}

だけど、実際に gidl.exe two_inv.idp | midl.exe と実行してみたら、midl.exe が「This application has requested the Runtime to terminate it in an unusual way. Please contact the application's support team for more information.」で落ちた。残念。

関連

• IDPで数独を解く - ヒビルテ(2009-03-04)
• The IDP framework for declarative problem solving - ヒビルテ(2009-08-13)

λ. ASPで 3 not problem を解いた

IDP (Inductive Definition Programming) でダメなら、解集合プログラミング(Answer Set Programming, ASP)でということで、やってみた。 ソルバには例によって、Potasscoで配布されているclingoを利用。入力は以下のようにした(two_inv.lp)。IDPの場合と違って、ASPの場合はプログラム全体が帰納的定義になっていて、欲しい結果がpに含まれない場合を一貫性制約(integrity constraint)を使って弾いている。

% domain predicate
bv8(0..255).

% inv(X)を満たすbv8(X)はたかだか2つ
0{inv(X) : bv8(X)}2.

p(15). % input 1 (15 = 0b00001111)
p(51). % input 2 (51 = 0b00110011)
p(85). % input 3 (85 = 0b01010101)
p(X & Y) :- p(X), p(Y), bv8(X), bv8(Y).
p(X ? Y) :- p(X), p(Y), bv8(X), bv8(Y).
p(~X & 255) :- p(X), inv(X), bv8(X).

% integrity constraint
:- not p(240). % output 1 (240 = 0b11110000)
:- not p(204). % output 2 (204 = 0b11001100)
:- not p(170). % output 3 (170 = 0b10101010)

これを clingo-2.0.3-win32.exe -n 0 two_inv.lp として実行した結果が two_inv_asp.txt 。オプションの -n 0 はモデルを全て列挙するという指定で、出力から inv(23), inv(105) なるモデルが唯一のモデルであることがわかる。 このnotを使う箇所は当然ながらOtterが見つけたものと同じものになっている。 このモデルから直接分かるのは、2つのnotを使う箇所だけだけど、ここから回路全体を構成するのは難しくない。

ASPすごいな、と初めて思ったよ。

関連

• ASPで数独を解く - ヒビルテ(2009-04-21)

λ. 何故ASPがすごいと思ったか補足

なんでASPがすごいかと思ったかというと、Pが帰納的(最小)であるという制約を除いたものを、有名なSMTソルバーであるYices(1.0.28)とCVC3(2010-07-11)に食わせてみて、ぜんぜん答えが出なかったので。

• test-yices.ys
• test-cvc3.cvc

λ. “Generic Programming with Adjunctions” by Ralf Hinze

2010-04-24 の Functional Programming Meeting 2010で紹介されていたもの。

Ψ : Nat(C(-,A), C(F-,A)) が与えらたときに、x ∘ in = Ψ x を満たす一意な x = (|Ψ|)_Id : μF→A が、Mendler-style fold (Mendler-style catamorphism) 。

これを拡張し、随伴 L ⊣ R と Ψ : Nat(C(L-,A), C(L(F-),A)) が与えられたときに、x ∘ L(in) = Ψx を満たす一意な x = (|Ψ|)_L : L(μF) → A を定義し、これを Adjoint fold と呼んでいる。 これは、随伴を Φ: C(LA, B) → D(A, RB) とすると、(|Ψ|)_L = Φ^-1 (|Φ ∘ Ψ ∘ Φ^-1 |)_Id という風に通常の Mendler-style fold に還元できる。

Adjoint fold の良いところは、引数にμFが直接現れずにコンテキストの中に現れているような再帰関数でも、そのコンテキストを表す関手が右随伴を持てば扱えること。 例えば、

append :: ([a], [a]) → [a]
append ([], ys) = ys
append (x:xs, ys) = x : (append xs ys)

を考えると、F(X) = Maybe (A, X) とおいて μF ≅ [a] で、L(X) = (X, μF) は右随伴 R(X) = (μF ⇒ X) を持つので、

Ψ : ∀X. (LX → μF) → (LFx → μF)
Ψ f (Nothing, ys) = ys
Ψ f (Just (a,x), ys) = a : f (x,ys)

append : (μF,μF) → μF
append = (|Ψ|)_L

という風に、Adjoint fold の形で書ける。

Fusion for adjoint folds から Type fusion へのつながりがイマイチよく分からなかった。 Fusion for adjoint folds が α(|Ψ|)_L = (|Ψ'|)_L' ⇐ α∘Ψ = Ψ'∘α なのに対して、 Type fusion が L(μF) ≅ μG ⇐ L∘F ≅ G∘L と、 νF ≅ R(νG) ⇐ F∘R ≅ R∘G で、 同じ形になっているのは分かるし、後者の証明に前者が使えるのもわかるのだけど、形の上での類似性だけで本質的な関係が何かあったりしないのだろうか?

Type fusion の証明は、以下で十分なのではないかと思った。 swap : L∘F ≅ G∘L が与えれているとき、ψ: GB→B に対して、Ψ ∈ Nat(C(L-,B), C(LF-, B)) を、Ψ(h) = ψ ∘ Gh ∘ swap とおくと、(|Ψ|)_L : LμF → B は h ∘ Lin_F = ψ ∘ Gh ∘ swap すなわち h ∘ Lin_F ∘ swap^-1 = ψ ∘ Gh を満たす一意な射なので、Lin_F ∘ swap^-1 は G の initial algebra 。

Type fusion を利用してのメモ化の導出も面白かった。

参考

• Categorical programming with inductive and coinductive types - ヒビルテ(2004-06-29)

λ. CLTT の 1.2 Some concrete examples: sets, ω-sets and PERs のノート

CLTT読書会で読んでいる、Categorical Logic and Type Theory の、1.2 Some concrete examples: sets, ω-sets and PERs を復習して、練習問題も一通り解いた。

• ノート

Exercise 1.2.7 の、ω-SetsとPERsのスライス圏での冪対象(exponential object)の作り方を、抽象的に圏論ぽくやる方法がわからず悔しい。何か方法があったような気もするのだけど。

λ. CLTT の 1.3 Some general examples のノート

CLTT読書会で読んでいる Categorical Logic and Type Theory の、1.3 Some general examples を復習して、練習問題も一通り解いた。

• ノート