論理としてのProlog (その2)
2022/12/22
2022/12/23 SWI-Prologのreverseの話題を分割した。
もう少し、Prologのプログラムで遊んでみようと思います。
[1] では、特定の値について、つまりrev([1,2,3], [3,2,1])だけの証明をしましたが、今回は、任意の値について証明してみましょう。
Coq/MathCompには、証明済みのappend ++や reverserev関数が用意されているので、それと同じ結果が得られることを証明するのが簡単だと思います。Coq/MathCompで用意されている補題を使うことができるからです。
この記事のソースコードは以下にありますが、実行にはCoq/MathCompは必要です。
From mathcomp Require Import all_ssreflect.
append の証明
簡単な例として、リストを連結するappendの証明をしてみます。Prologでは、append述語
appendは、次のように定義されます。ここではλPrologのstdlibから採っています。
pred append i:list A, i:list A, o:list A.
append [X|XS] L [X|L1] :- append XS L L1 .
append [] L L .
Variable T : Type.
Lemma rev_nil : @rev T [::] = [::].
Proof.
done.
Qed.
Module LApp.
今回は、Coqで扱い易いように、PrologのプログラムをHypothesisとして定義します。
Variable append : list T -> list T -> list T -> Prop.
Hypothesis ap1 : forall (X : T) (XS L L1 : list T),
append XS L L1 -> append (X :: XS) L (X :: L1).
Hypothesis ap2 : forall (L : list T), append [::] L L.
Prologのプログラムappendの第1引数(XS)と第2引数(L)に対して、これらを連結したものが、第3引数のXS ++ Lになることを証明します。
Prologのプログラムと同様に、appendの第1引数のリストについての帰納法で証明します。
Theorem app3_app XS L : append XS L (XS ++ L).
Proof.
elim: XS => /= [| X XS IH].
- by apply: ap2.
- by apply: ap1.
Qed.
End LApp.
reverse の証明
[1]でも取り上げたreverseについて証明します。Prologの述語とCoq/MathCompの関数名が重複してしまうので、Prologの述語のほうをrev2と改名しています。それ以外は、Hypothesisとして定義したことを除いて、変わりはありません。
pred rev2 i:list A, o:list A.
rev2 L RL :- rev3 L [] RL.
rev3 [X|XS] ACC R :- rev3 XS [X|ACC] R.
rev3 [] L L.
Module LRev.
Variable rev2 : list T -> list T -> Prop.
Variable rev3 : list T -> list T -> list T -> Prop.
Hypothesis rv0 : forall L RL, rev3 L [::] RL -> rev2 L RL.
Hypothesis rv1 : forall X XS ACC RL,
rev3 XS (X :: ACC) RL -> rev3 (X :: XS) ACC RL.
Hypothesis rv2 : forall RL, rev3 [::] RL RL.
ループ不変式
補助述語rev3が定義されているため、証明はちょと複雑になります。rev3の実行をトレースしてみます。
enter: rev3([1,2,3], [], RL)
enter: rev3([2,3], [1], RL)
enter: rev3([3], [2,1], RL)
enter: rev3([], [3,2,1], RL)
exit: rev3([], [3,2,1], [3,2,1])
exit: rev3([3], [2,1], [3,2,1])
exit: rev3([2, 3], [1], [3,2,1])
exit: rev3([1, 2, 3], [], [3,2,1])
rev3の、第1引数をreverseして第2引数にappendしたものが第3引数になっているようです。このことを証明してみましょう。
これは常に成り立つので「ループ不変式」といいます。途中で、MathCompのrevと++関数について、
rev (a :: A) ++ B = rev A ++ (a :: B) であることを証明する必要が生じましたが、MathCompの補題で証明できました。
Lemma rev3_invariant A B : rev3 A B (rev A ++ B).
Proof.
elim: A B rv1 rv2 => //= a A IHA B Hcons Hnil.
apply: (Hcons).
have -> : rev (a :: A) ++ B = rev A ++ (a :: B)
by rewrite -[a :: A]cat1s rev_cat -catA.
by apply: IHA.
Qed.
rev3 についての補題
rev3 について、第1引数をreverseしたものは第3引数であることは、さきの補題の特殊な場合として、簡単に証明できます。
Lemma rev3_rev L : rev3 L [::] (rev L).
Proof.
rewrite -[rev L]cats0.
by apply: rev3_invariant.
Qed.
証明したかった定理
証明したいのは、2引数のrev2についてですが、これも上の命題からから簡単に証明できます。
Theorem rev2_rev L : rev2 L (rev L).
Proof.
apply: rv0.
by apply: rev3_rev.
Qed.
End LRev.
もうすこし複雑なプログラム
もう少し複雑なプログラムを証明してみましょう。といっても、append述語を使ってreverseを定義した述語です。証明の過程で、最初に証明したapp3_appを使用しています。
reverse [X | XS] L2 :-
reverse XS L,
append L [X] L2.
reverse [] [].
Module Rev2.
Variable rev2 : list T -> list T -> Prop.
Hypothesis rv1 : forall (X : T) (XS L L2 : list T),
rev2 XS L -> LApp.append L [:: X] L2 -> rev2 (X :: XS) L2.
Hypothesis rv2 : rev2 [::] [::].
Theorem rev2_rev XS : rev2 XS (rev XS).
Proof.
elim: XS => /= [| X XS IH].
- rewrite rev_nil.
by apply: rv2.
- apply: rv1.
+ by apply: IH.
+ rewrite -[X :: XS]cat1s rev_cat.
by apply: LApp.app3_app.
Qed.
End Rev2.
おまけ
reverseの別の定義である、SWI-Prologの実装例については、[2]を参照してください。
まとめ
証明の説明は省いたため、Coqに親しみのない場合は難しいと思いますが、論理型言語Prologであっても、プログラムとしての証明は、それほど簡単ではなく、とくに、実装によって証明が全く変わることなど、手続き型言語や関数型言語と違いは大きくないと、言えるのではないでしょうか。
文献
[1] 論理としてのProlog
https://qiita.com/suharahiromichi/items/c4427a21a7d11f468e39
[2] SWI-Prolog の Reverse述語
https://qiita.com/suharahiromichi/items/37de0c79f043836199b6