TPP 2024: 20th Theorem Proving and Provers Meeting


English version

第20回 TPPミーティングを 11月 25日(月)-26日(火) に九州大学にて開催します.
このミーティングは,2005年から年に1回開催され, 定理証明系を作っている人から使う側の人まで幅広い人たちが集まり, 様々な側面からの話をしてアイディアの交換をしてきたものです. なお,今年は招待講演者としてフランスINRIA の Pierre-Marie Pédrot を 呼んでいます. Coqの内蔵について講演する予定です.

開催情報

日時:11月25日(月) 13:00 〜 11月26日(火) 15:00
場所:九州大学 マス・フォア・インダストリ研究所
  九州大学 伊都キャンパス ウエスト1号館 D棟 4階 IMIオーディトリ アム(W1-D-413)
IMIのイベ ントページ
ハイブリッドでの開催を予定していますが,九州大学まで来られるとうれしいです.

参加申込

参加は無料です. この 参加登録フォー ム をご記入下さい.
申込は11月20日まででお願いします.同時に発表を申し込む場合は,なるべく 11月11日まででお願いします.

学生・若手講演者への旅費支援について

今回のTPP2024は, 共共拠点「産業数学の先進的・基礎的研究拠点」の プロジェクト研究・短期共同研究として開催されます. 今回のTPP2024参加にて, 旅費の支援を希望される方は, 参加申込フォーム[その他ご要望]欄にて, ご連絡下さい. 限られた拠点予算の範囲になりますので, ご希望に添えない場合もあります. あらかじめ, ご了承下さい.

会議録について

今回のTPP2024は, IMI共共拠点研究集会として開催されます. ご講演者には, 発表スライドの抜粋でも構いませんので, 記録となる資料を 提出して下さい. 九大IMIのLecture Noteシリーズの1巻として発行します. ご協力のほど,よろしくお願いいたします.

懇親会

懇親会場: ざうお糸島本店 (お魚が美味しいお店です)
https://zauo-itoshimahonten.owst.jp/
宴会日時: 11月25日(月) 18:30 - 20:30
会費: 5000円 (飲み放題コース)

ホテル情報

グローカルホテル糸島
九大伊都キャンパスからバスで6分・九大関係者割引あり(シングル8800円)
HOTEL AZ 福岡糸島
JR「糸島高校前」そば,「浦志」バス停から「九大工学部」バス停まで, バスで約15分.

TPPmark

今年のTPPmarkは互換による整列をテーマにしています.この場合,整列のコ ストは比較の数ではなく,整列するのに必要な互換の数です.

例えば,リスト [5, 9, 1, 3, 7] を整列するには,すなわちリスト [1, 3, 5, 7, 9] に変えるには,3つの互換を適用すればいい.まず位置1と3を交換し, 次に2と4を交換し,しまいに4と5を交換すればいい(ただし位置を1から数えた 場合). 別の見方をすれば,置換 [1 → 3, 2 → 5, 3 → 1, 4 → 2, 5 → 4] を適用する必要がある.線形代数の講義を思い出すと,置換はまず循環に分解 できる.ここでは (1 3) と (2 5 4) である (循環内に各位置が次のものにな り,最後の位置が最初のものになる).そして循環がまた互換に分解される. 長さmの循環が(m-1)互換で実現できるので,最適なアルゴリズムが (要素の数 - 循環の数) 個の互換で整列を完成させる.

タスクは以下のとおりである.

  1. 置換をその置換を実現する最小の互換の列に変換する関数を書きなさい.
  2. この関数の正しさ,そして列の最小性を証明せよ. この際,置換に関する理論が必要だろう.
  3. 重複のない自然数のリストを与えられたら,それを整列する最小の互換列を返す関数 を書きなさい.正しさと列の最小性を証明せよ.
  4. 重複のありうる自然数のリストを与えられたら,それを整列する最小の互換列を返す関数 を書きなさい.正しさと列の最小性を証明せよ.
位置を0から始めてもよい.

問い合わせ先

質問およびTPPmarkの回答は題名にTPPを含め,Jacques Garrigueまで送って下さい.
garrigue at math.nagoya-u.ac.jp


The 20th Theorem Proving and Provers meeting will be held on November 25(Mon) - 26(Tue), 2024 at Kyushu University.
TPP is held every year since 2005, and provides a forum to exchange ideas for both users and implementors of theorem provers and proof assistants. This year our invited speaker is Pierre-Marie Pédrot of INRIA Atlantique (France), and he shall tell us about Coq bowels.

Information

Time: 11/25 1pm to 11/26 3pm
Place: Kyushu University, Institute of Mathematics for Industry
  IMI Auditorium (W1-D-413), West Zone 1, Ito campus, Kyushu University
Event page at IMI
We plan to allow remote access to the talks, but please consider coming to Kyushu University.

Registration

Attendance is free. Please fill this Registration Form.
Please register before November 20th. If you plan to give a talk, I would be grateful if you register by November 11th.

Travel expenses support for students and young speakers

If you would like to apply for travel expenses for participation in this year's TPP2024, please contact us in the [Other Requests] section of the registration form. Please note that due to the limited budget of the centre, we may not be able to meet your request. Thank you for your understanding.

Proceedings

This year's TPP2024 will be held as a meeting in the joint research meeting center for advanced and fundamental mathematics-for-industry. Please submit materials that will be used as records, even if it is a subset of the presentation slides used in your talk. It will be published as a volume of the Lecture Note series of IMI, Kyushu University. We would appreciate your cooperation.

Party

Location: Zauo Itoshima-Honten (Fish restaurant)
https://zauo-itoshimahonten.owst.jp/
Date: 11/25(Mon) 18:30 - 20:30
Fee: 5000 yens (drinks included)

Hotel

Glocal Hotel Itoshima
Close from Kyushu U. Ito Campus. Reduced rate for persons going to Kyushu U. (Single from 8800 yens)
HOTEL AZ Fukuoka-Itoshima
15 minutes by bus to Kyushu U. Ito Campus.

TPPmark

This year's TPPmark is about an optimal in-place sorting algorithm, but where values can only be moved by exchanging the contents of two locations. As a result, the definition of cost is not the number of comparisons but rather the number of exchanges.

For instance, if we want to sort the list [5, 9, 1, 3, 7], i.e. convert it into the list [1, 3, 5, 7, 9], we can do it by 3 exchanges, of positions 1 and 3, 2 and 4, and 4 and 5 (indices starting from 1). Another way to see it is that you need to apply the permutation [1 → 3, 2 → 5, 3 → 1, 4 → 2, 5 → 4]. Now you might recall from your linear algebra course that such a permutation can be decomposed into cycles (here (1 3) and (2 5 4), where each position moves to the next one in the cycle, and the last one to the first), which can themselves be decomposed into exchanges (aka transpositions). Since a cycle of length m can be represented by (m-1) exchanges, the optimal algorithm requires (number of elements - number of cycles) exchanges.

The task are as follows:

  1. Define a function which, given a permutation, returns the a minimal sequence of exchanges which realizes it.
  2. Prove that this function is correct, and that the number of exchanges is minimal. This will probably require building a theory of permutations.
  3. Define a function which, given a list of natural numbers without repetition, returns a minimal sequence of exchanges which sorts it. Prove it correct and minimal.
  4. Define a function which, given a list of natural numbers possibly with repetitions, returns a minimal sequence of exchanges which sorts it. Prove it correct and minimal.
You may use indices starting from 0 rather than 1.

Questions

Send your questions and TPPmarks answers to Jacques Garrigue (with TPP in the subject).
garrigue at math.nagoya-u.ac.jp

これまでのTPP / Past TPPs

TPP2023 / TPP2022 / TPP2021 / TPP2020 / TPP2019 / TPP2018 / TPP2017 / TPP2016 / TPP2015 / TPP2014 / TPP2013 / TPP2012 / TPP2011 / TPP2010 / TPP2009 / TPP2008 / TPP2007 / TPP2006 / TPP2005


Last update: November 19, 2024.