12th Theorem Proving and Provers (TPP 2016)

浅井健一 / Kenichi Asai
お茶の水女子大学 / Ochanomizu University

November 14 (Mon) to 15 (Tue), 2016

Abstract: TPP (Theorem Proving and Provers) ミーティングは、2005 年から年に１回開催され、定理証明系を作っている人から使う側の人まで幅広い人たちが集まり、様々な側面からの話をしてアイディアの交換をしてきたものです。

ミーティング期間中の討論を大切にしたいと考えていますので、出来上がった仕事の講演だけでなく、進行中の仕事、未完成の仕事についての講演も歓迎します。参加者には可能な限りご講演いただきたいと希望しています。

1 日時・場所 / Date, Venue

日時: 2016 年 11 月 14 日（月）10:40 頃から 15 日（火）12:00 頃まで（予定）
Date: Monday, November 14, around 10:40 to Tuesday, November 15, around 12:00.
場所: お茶の水女子大学理学部 3 号館 2 階 209 会議室（地図の 20 番の建物）
Venue: Ochanomizu University, Faculty of Science Building No. 3, 2nd floor, meeting room 209. (The building No. 20 in this map.)
住所: 112-8610 東京都文京区大塚 2-1-1
Address: 112-8610, 2-1-1 Otsuka, Bunkyo-ku, Tokyo
懇親会 Dinner party: 2016 年 11 月 14 日（月）18:00 から食彩酒席ビカヴォ（東京都文京区大塚3-1-12 コダマビル 1F, 03-5977-1717）

2 プログラム / Program

参加者: 37 名程度。（うち懇親会参加者 20 名。）

3 TPPmark

今年は、趣向を少し変えて、依存型プログラミング系の問題を出題します。

3.1 問題（依存型プログラミング的な表現）

引数として以下の３つ

リストのリスト lst
整数 i
整数 j

を受け取ったら、 lst の i 番目のリストの j 番目の要素を削除したものを返す関数 remove-lst を作成せよ。その際、以下の３つの条件

lst の i 番目のリストが存在する。
i 番目のリストの j 番目の要素が存在する。
返されるリストたちの長さは、i 番目のみ 1 短くなっており、他は変わらない。

が保証されるようにせよ。（ここで、先頭はいずれも 0 番目とする。）

3.2 問題（論理的な表現）

以下の３つのデータがある。

リストのリスト lst
整数 i
整数 j

このとき、lst の i 番目のリストの j 番目の要素を取れるならば、以下を満たすリストが（唯一）存在することを示せ。

lst の中の

i 番目のリストについては、その j 番目の要素を取り除き、
それ以外のリストについては、もとのまま

であるようなリストで、返ってくるリストたちの長さは、

i 番目のリストについては、もとのリストより 1 短くなっており、
それ以外については、もとのリストと同じ

になっている。（ここで、先頭はいずれも 0 番目とする。）

3.3 OCaml によるプログラム

この問題（の依存型プログラミング表現の方）を（３つの条件を満たさない形で）OCaml を使って書くとremove.ml のようになります。（プログラム中のテストが、プログラムの入出力の具体例になっています。）このプログラム中、２か所に現れる raise CannotHappen となるケースを、上手に引数に条件を加えることで、起こり得ないようにするとともに、返ってくるリストの長さが所定のところのみ 1 小さくなっていることを示してくださいと言うのが問題の趣旨です。

２か所の例外は、どちらもリストの長さを考慮すれば簡単に削除できそうに見えます。 lst の長さを n、 lst 中の各リストの長さを順に m₀,...,m_n-1 としましょう。すると i は 0 から n-1 までの整数、 j は 0 から m_i-1 までの整数とすれば良いでしょう。ここで問題となるのは j の範囲が m_i（したがって i）に依存しているところです。それをうまく書けるかどうかが知りたいです。

3.4 問題の背景

項の単一化を行う際には、メタ変数に項を代入します。例えば SK 論理の式 SXK(YKZ)K があったとしましょう。ここで X, Y, Z はメタ変数です。この式のメタ変数 Y に S を代入すると SXK(SKZ)K が得られます。この代入の操作の際、メタ変数は [X; Y; Z] の３つから [X; Z] のふたつに減っています。この操作が、上の問題で lst の長さが 1 の場合に対応しています。つまり、lst の 0 番目のリストの 1 番目の Y を削除し、残ったメタ変数のリストを返しています。

この例では「SK 論理の式」というひとつの概念のみを扱っていたので、メタ変数もそれを表す１種類のみでした。上の問題は、項の種類を複数に拡張し、相互再帰している場合に対応しています。今、項が n 種類からなり、それらが相互再帰しているとします。 n 種類の項に対応したメタ変数がそれぞれ m₀,...,m_n-1 個あったとしましょう。この状態で、i 番目の項の j 番目のメタ変数に代入を行うと、代入後のメタ変数は、そのひとつだけが削除された形になります。

現在、このような形でメタ変数の数を管理しながら項の単一化のプログラムを書こうとしているのですが、相互再帰してメタ変数の種類が複数になった場合、どのようにして良いのかわからなくなり、皆さんのお知恵を借りたいと思った次第です。

3.5 寄せられた解答

OCaml (!): Garrigue さん
Agda: 松本・山田さん
Coq 系: Garrigue さん、森口さん、井上さん、池渕さん、佐藤さん、山本さん、小島さん

4 過去の TPP / Past Workshops

This document was translated from L^AT_EX by H^EV^EA.