再帰的余代数について

最近、再帰的余代数という概念について少し勉強したので、証明をまとめてPDFにした。

github.com

動機など細かいところには触れられていないが、以下のことが証明されている。

  • 再帰的余代数 = 始代数
  • Setでは、再帰的ならば整礎

WSL+Xming環境整備

WSLとXmingを組み合わせていい感じに環境整備できてきたので記録をとる。

WSLとXmingについて

  • WSLはWindows上でLinuxのプロセスを実行する機能である。互換性は完全ではないが、多くのソフトウェアが動くようになっている。ただし、そのままではGUIは動かない。
  • XmingWindows上で動作するXサーバーのうちの一つ (Cygwin/Xの派生) である。XはLinuxで使えるGUIの仕組みで、画面側がXサーバー、アプリ側がXクライアントとなってTCP経由で接続できるという特徴がある。ここではWSL側をクライアントにしてXmingに繋ぐことで、GUIを使えるようにする。

Xming最新版の取得

Xmingの最新版のビルドを入手するには£10.00程度の寄付が必要である。多くの人は2007年(!!!)のバージョンを使っている。そういうわけなので巷の評判は気にせず最新版を入手するといいと思う。 (たとえば、勝手に英語キーボード設定になる問題には今のところ遭遇していない)

同ページの寄付に関するセクションに詳しい説明がある。以下は勝手に翻訳したもの

寄付をすると、ドナーパスワードがメールで送られます。それを使うことで、XmingのWebリリース版と開発スナップショット版を個人利用のために取得することができます。パスワードは、PayPalの支払い履歴に記載されているメールアドレスに対して送られます。そのため、支払いメールアドレスが有効なメールアドレスであることと、私のISPのメールサーバー ([WWW]zen.co.uk 、例えば smarthost01.mail.zen.net.uk) をブロックしていないことを確認しておいてください。寄付以外の方法(コードやパッチなど)で貢献をした場合や、パスワードが送られてこない場合は、私に連絡をしてください。また、PayPalを使えず、代替手段が必要な場合も、私にメール (訳注: ここにメールアドレスが書いてあります) で連絡をしてください。寄付金額として10ポンドを提案していますが、これより低い金額だと手数料の割合が高くなってしまうからです。注意: 上のボタンを経由してPayPalで支払いをする場合、PayPalのアカウントは必要ありませんが、クッキーを有効にする必要があります。

寄付はPayPal経由と書いてあるが、PayPalは日本からの寄付を許可していない(おそらく法的な理由)。その場合は上にあるように作者にメールをするとよい。以下は筆者の送ったメールの例

Subject: Want to donate from Japan

Text:

I want to donate to Xming from Japan, from which I can’t donate money via PayPal due to legal reasons. Could you offer alternatives if any?

Masaki Hara

すると代替手段を教えてもらえる。筆者は、作者からPayPalの支払いリンクを送ってもらう方法(日本から寄付はできないが、支払いはできる)を選んだ。

Subject: Re: Re: Want to donate from Japan

Text:

Thank you! Can I receive a payment link then?

しばらくするとPayPalの支払いリンクを送ってもらえるので、それに対して£10.00支払うと、パスワードが送られてくる。

Xmingのインストール

今回はWSLから呼び出す形での利用のみを想定しているのでPuTTY連携は考えない。そのため以下の2つをインストールする。

Xming-fontsはXming-x64のあとにインストールする。逆順にすると C:\Program Files (x86)\Xming にインストールしようとしてしまう。

ちなみにこのXming-fontsだが、ほぼEmacs用である。GTKやQtなどで作られているGUIアプリはクライアント側(Linux側)のフォントを参照するからである。

Xmingの起動

はじめはXming Launchなどを使って起動してみるとよいが、オプションがわかってしまったあとはショートカットを作るほうが楽だ。

"C:\Program Files\Xming\Xming.exe" :0 -clipboard -multiwindow -xkbmodel jp106 -xkblayout jp -dpi auto -wgl へのショートカットを作成した。

  • :0 は画面の番号で、これに6000を足したTCPポートで通信が行われる。
  • -clipboard によりWindows側のクリップボードと共有する。
  • -multiwindowXmingのモードの一つで、Linux側のウインドウ1個がWindows側のウインドウ1個に対応する。
  • -xkbmodel jp106 -xkblayout jp は日本語キーボード配列を指定している。
  • -dpi autoWindows側のDPIを継承する。筆者のコンピューターはNew Surface Proで、高DPI環境だが、この設定だけでかなりうまく設定される。
  • -wglOpenGLアクセラレーションを有効化する。

WSLの設定 (Ubuntuのインストール)

Bash on Ubuntu on Windowsをインストールしてみよう! - Qiita」に従ってWSLを設定した。WSLの上では他のディストリビューションも動かせるが、ここではUbuntuを仮定する。

Xfce4のインストール

bash.exeを起動して xfce4-sesson, xfce4-goodies, gnome-keyring, fonts-vlgothic, fcitx-skk をインストールした。 (ここで日本語フォントを入れておかないと、Xming-fontの有無に関係なく日本語が化けて困ることになる)

起動スクリプトの作成

以下のような内容のスクリプトを /home/qnighy/Xming.sh に置いた。

#!/bin/bash

# ホームから開始したいので
cd
# パーミッション777のファイルが量産されると困るので
umask 0022
# localhost:0.0の略で、これでXmingに繋がることになる
export DISPLAY=:0.0
# 必ずXming経由でOpenGLを使う
export LIBGL_ALWAYS_INDIRECT=1

# gnome-keyringをスタート (SSH鍵を覚えさせたいので)
eval $(gnome-keyring-daemon --start --components=pkcs11,secrets,ssh)
export GNOME_KEYRING_CONTROL SSH_AUTH_SOCK

# インプットメソッドの設定 (fcitxの場合)
IM=fcitx
export XMODIFIERS="@im=$IM"
export GTK_IM_MODULE=$IM
export QT_IM_MODULE=$IM
export NO_AT_BRIDGE=1
# 全角/半角キーが連打される例のやつを防ぐ
xset -r 49
# fcitxを起動
fcitx

# SHLVLを0に下げてからターミナルを起動
SHLVL=0 xfce4-terminal

bash.exe -l /home/qnighy/xming.sh のように実行するとターミナルが出てくる。やっほい

ショートカットの作成

bash.exeを黙らせたいので、無言で実行するためのユーティリティーを導入する。

The Run utilityからrun-x64.zipをダウンロードして、中にあるrun.exeC:\Windows\System32\にコピーする。 (Xmingの作者が作っている模様)

その後、 C:\Windows\System32\run.exe C:\Windows\System32\bash.exe -l /home/qnighy/xming.sh に対してショートカットを作成する。

アイコンをいい感じにする

Xmingの作るウインドウは、極力Linux側のアイコンを反映するが、上手くいかないことがある。特にxfce4-terminalは上手くいかなかったので、手動で設定する。

まず imagemagick を入れて、以下のようにしてicoファイルを作成する。

convert /usr/share/icons/elementary-xfce/apps/*/xfce-terminal.png xfce-terminal.ico

同じ方法で色々なアイコンをicoに変換できる。

作ったicoWindows側に置く。まずショートカットが不恰好なのでショートカットのアイコンに設定する。

続いてXmingrcをいじる。Xmingrcのデフォルト設定は C:\Program Files\Xming\Xmingrc にあるので、これを C:\Users\qnighy\Xmingrc にコピーする。

# Xming Server Default Resource File
# follow.exe and xhost.bat are in "Tools and clients"
Menu apps {
    "&View the log" viewlog
    "&Tail the log" execd follow
    "&Reload Xmingrc" reload
    &Usage execd "Xming :999 -help"
    "Access Control &Status" execd "xhost.bat"
    "&Command Prompt" execd cmd
    "Host &Finder" finder
    separator
}
RootMenu apps
SilentExit
Debug "Using the default Xmingrc configuration file."

これを弄って以下のようにした。

# Xming Server Default Resource File
# follow.exe and xhost.bat are in "Tools and clients"
Menu apps {
    "&View the log" viewlog
    "&Tail the log" execd follow
    "&Reload Xmingrc" reload
    "&Usage" execd "Xming :999 -help"
    "Access Control &Status" execd "xhost.bat"
    "&Command Prompt" execd cmd
    separator
}
RootMenu apps
SilentExit
Icons {
    # アイコンを上書き
    xfce4-terminal C:\Users\qnighy\xfce-terminal.ico
}

こうするとウインドウクラスかウインドウ名がxfce4-terminalであるようなウインドウには、指定したアイコンを使うようになる (Xmingrcの説明も参照)

ところで、ウインドウクラスを調べるには xprop コマンドを使う。 xprop を実行したあと、調べたいウインドウをクリックすると、以下のように色々な属性が表示される。

$ xprop
_NET_WM_STATE(ATOM) = 
_NET_WM_USER_TIME(CARDINAL) = 3901640
_WINDOWSWM_NATIVE_HWND(INTEGER) = 328280, 0
WM_STATE(WM_STATE):
        window state: Normal
        icon window: 0x0
WM_HINTS(WM_HINTS):
        Client accepts input or input focus: True
        Initial state is Normal State.
        window id # of group leader: 0xe00001
XdndAware(ATOM) = BITMAP
_MOTIF_DRAG_RECEIVER_INFO(_MOTIF_DRAG_RECEIVER_INFO) = 0x6c, 0x0, 0x5, 0x0, 0x0, 0x0, 0x0, 0x0, 0x0, 0x0, 0x0, 0x0, 0x10, 0x0, 0x0, 0x0
WM_WINDOW_ROLE(STRING) = "xfce4-terminal-1506224785--565597661"
_NET_WM_SYNC_REQUEST_COUNTER(CARDINAL) = 14680070
_NET_WM_WINDOW_TYPE(ATOM) = _NET_WM_WINDOW_TYPE_NORMAL
_NET_WM_USER_TIME_WINDOW(WINDOW): window id # 0xe00005
WM_CLIENT_LEADER(WINDOW): window id # 0xe00001
_NET_WM_PID(CARDINAL) = 20
WM_LOCALE_NAME(STRING) = "ja_JP.UTF-8"
WM_CLIENT_MACHINE(STRING) = "qnighy-chris"
WM_NORMAL_HINTS(WM_SIZE_HINTS):
        user specified size: 362 by 0
        program specified minimum size: 93 by 116
        program specified resize increment: 19 by 38
        program specified base size: 17 by 40
        window gravity: NorthWest
WM_PROTOCOLS(ATOM): protocols  WM_DELETE_WINDOW, WM_TAKE_FOCUS, _NET_WM_PING, _NET_WM_SYNC_REQUEST
WM_CLASS(STRING) = "xfce4-terminal", "Xfce4-terminal"
WM_ICON_NAME(STRING) = "Terminal - xprop"
_NET_WM_ICON_NAME(UTF8_STRING) = "Terminal - xprop"
WM_NAME(STRING) = "Terminal - xprop"
_NET_WM_NAME(UTF8_STRING) = "Terminal - xprop"

このうち WM_CLASS と書かれているものがウインドウクラスにあたる。はじめから xprop | grep WM_CLASS とやると楽かもしれない。

困っていること

  • dbusがうまく動かない。redditとかに色々書いてあるけど手元ではまだ動いていない。
  • OpenGLで複雑なことをしようとすると厳しい。なぜかGLSLのコンパイルが通らない。
  • 他にも変なシステムコールは通らないので、そういうことをやるときは仮想マシンを立ち上げる。

古いRubyをビルドする

動機

現時点でRubyの最新版は2.4, サポートされているのは2.2までで、2.1以前はメンテナンス対象外である。そのような古いバージョンを動かすのは決してよいことではない。

しかし実のところ、現在でも多くのWindowsマシンで、Ruby1.8.1とRuby1.9.2p0が動作している。具体的には、RPGツクールXP, RPGツクールVXというソフトウェアで作られたゲームはRuby1.8.1の処理系とともに配布されており、RPGツクールVX Aceというソフトウェアで作られたゲームはRuby1.9.2p0の処理系とともに配布されている。既に多くのゲームが世に送り出されているのみならず、これらのいずれのツールも、未だにそれぞれ根強い人気があり、今でも多くの名作が作られている。「ふりーむ」というサイトで「RPGツクール XP」と検索した結果からも、その人気を伺い知ることができる。

そういった事情から筆者はRuby1.8.1とRuby1.9.2p0に強い興味があり、ビルドを試みたところ、いくつかの問題があった。

前提

とりあえず、Ubuntu 16.04 x86_64でのビルドを想定している。アーキテクチャを拡大すれば、より多くの問題が顕在化するかもしれない。

Ruby1.9.2p0の問題

Ruby1.9.2p0を現代の環境でビルドすると、以下の問題があった。

  • 継続・コルーチン処理が最適化で壊れる
  • bisonでコンパイルエラーになる

継続・コルーチン処理が最適化で壊れる

Fiberやcall/ccの処理はスタックのコピーによって実現されているが、コンパイラによってはspレジスタの最適化によりこの処理が壊れてしまい、処理系がサイレントに死ぬことがある。これはr34278をbackportすることで解決できた。

bisonでコンパイルエラーになる

pure-parser周りの仕様変更により新しめのbisonでコンパイルできない。これはr42282をbackportすることで解決できた。

Ruby1.8.1の問題

Ruby1.8.1を現代の環境でビルドすると、以下の問題があった。

  • group_memberの衝突
  • bisonとの組み合わせでGCが壊れる
  • autoconf2.6x系列でビルドできない

group_memberの衝突

file.cで定義されているgroup_memberと、Cライブラリのgroup_memberが衝突する。これはgroup_memberrb_group_memberにリネームすることで解決できた。歴史的にはこの変更はr13240r26682の組み合わせといえる。

bisonとの組み合わせでGCが壊れる

ある程度新しいbisonはLRのセマンティックバリューのスタックをヒープで管理することがあるが、この場合Ruby1.8.1だとヒープ上のセマンティックバリューのマーク漏れが発生する。ノードのnd_fileが汚染された結果、次のGCのタイミングでGCのフリーノードの直前のRVALUEの最後の1バイトが破壊され、その1バイトがノードからのポインタになっていた場合に領域外参照でサイレントに死ぬ。これはr9355, r9405, r9416, r9382, r9639をbackportすることで解決できた。

autoconf2.6x系列でビルドできない

いくつかの複合的な問題からautoconf2.6系列でビルドできない。これはr10189の一部、r10392r11594をbackportして、srcdirの解釈を正しくするよう少し改造を加えることで解決できた。

成果物

現時点での成果物をqnighy/ruby-1.9.2p0qnighy/ruby-1.8.1に置いてある。

Rust-proofを使ってみる

概要: Rust-proofはElectrolysisと同様にRustプログラムから検証条件を抽出するが、LeanではなくSMTソルバであるZ3向けの検証条件を出力する。こちらも開発が放棄されているように見えるが現在もビルド可能である。

準備

テスト用リポジトリを準備する

$ cargo new rustproof-test
$ cd rustproof-test

該当のnightlyバージョンを取得する (Electrolysisと同様、Rust-proofもコンパイラプラグインのため、特定のnightlyバージョンに強く依存している)

$ rustup override set nightly-2016-08-12

Z3をインストール

$ sudo apt install z3

使ってみる

Cargo.toml に以下の依存関係を書く

[dependencies]
rustproof = { git = "https://github.com/Rust-Proof/rustproof.git", rev = "654b004" }

src/lib.rs に以下のように関数を書く。これはEXAMPLESに掲載されているものとほぼ同様だが、5:i32のような型つきリテラル5i32に置き換えてある。

// feature(plugin) を有効化してrustproofをロード
#![feature(plugin)]
#![plugin(rustproof)]

// #[condition] によりコンパイル時にrustproofによるチェックが走る

#[condition(pre="(x:i32 <= i32::MAX - 5i32)", post="return:i32 == (x:i32 + 5i32)")]
pub fn add_five(x:i32) -> i32 {
    assert!(x <= 2147483647-5);
    x+5
}

#[condition(pre="(x:i32 <= i32::MAX - 4i32)", post="return:i32 == (x:i32 + 5i32)")]
pub fn add_five_invalid(x:i32) -> i32 {
    assert!(x <= 2147483647-5);
    x+5
}

#[condition(pre="true", post="(x:bool==true IMPLIES return:bool==false) && (x:bool==false IMPLIES return:bool==true)")]
pub fn boolean_not(x:bool) -> bool {
    if x == true {
        false
    } else {
        true
    }
}

検証を実行するには単にコンパイラを起動すればよい。

$ cargo build
   Compiling rustproof-test v0.1.0

fn add_five(..) Verification Condition is valid.


fn boolean_not(..)  Verification Condition is valid.


fn add_five_invalid(..) Verification Condition is not valid.

(model 
  (define-fun x () (_ BitVec 32)
    #x7ffffffb)
)

    Finished debug [unoptimized + debuginfo] target(s) in 42.84 secs

まとめ

大変よい試みだが、古すぎるのが残念だと思う。rust-proofが開発された経緯は不明だが、documentsというディレクトリに不穏な資料が残されているので見てみると面白いかもしれない。

Electrolysisを使ってみた

概要: ElectrolysisはRustの検証条件をLEANに出力するプロジェクトである。これを使ってみた。

Electrolysisとは

Electrolysis (electrolysis: 電解) はSebastian Ullrich氏の修士研究で開発されたプロジェクトで、Rustプログラムの正当性や計算量に関する検証条件をLean Theorem Proverの命題として出力する機能を提供する。

なお、GitHubの様子だと、このプロジェクトは修論の日付からほぼ開発がストップしているようだ。Ullrich氏はその後、Electrolysisの成果の一部をLEANに還元するなどの活動をしているようだ。

Electrolysisの実行

以下、Ubuntu 16.04を仮定する。

ElectrolysisはRustのコンパイラプラグインとして実装されているため、Rustの特定のnightlyバージョンに強く依存している。また、libcore自体を検証ターゲットにしているため、Rustコンパイラソースコード自体も取得する必要がある。

$ git clone https://github.com/Kha/electrolysis.git
$ cd electrolysis
$ rustup override add $(cat rust-nightly-version)
$ rustup component add rust-src
$ cargo run core
$ cargo run alloc
$ cargo run collections
$ cargo run fixedbitset

petgraphに対する検証条件の出力

petgraphに対する検証条件の出力はやや面倒である。まずpetgraphを取得してビルドする。

$ git submodule update --init
$ cd thys/petgraph/src
$ cargo build
$ cd ../../..

次に thys/petgraph/config.toml を編集して、libfixedbitsetのrlibのハッシュを適切に置き換える。例えば、

rustc_args = "thys/petgraph/src/src/lib.rs --crate-name petgraph --crate-type lib -L dependency=thys/petgraph/src/target/debug/deps --extern fixedbitset=thys/petgraph/src/target/debug/deps/libfixedbitset-0ba3fe99bd419295.rlib"

targets = [
  "algo.scc",
]

とすると以下が通る。

$ cargo run petgraph

Lean2のビルド

Leanは現在、過去の証明との互換性のために残されている0.2.0系列と、最新の3.0.0系列がある。Electrolysisに適しているのは0.2.0系列なので、そちらを使う。

また、lean2のビルドスクリプトにはninjaを取得する部分があるが、ninjaの取得先が削除されてしまっているので、以下のパッチを当てる必要がある。(以下これをlinja.patchと呼ぶ)

diff --git a/bin/linja.in b/bin/linja.in
index 926f33e..10ee37d 100755
--- a/bin/linja.in
+++ b/bin/linja.in
@@ -239,7 +239,7 @@ def show_download_progress(*data):
     log_nonewline("Download: size\t= %i kb, packet: %i/%i" % (file_size, downloaded_packets, total_packets+1))
 
 def get_ninja_url():
-    prefix = "https://leanprover.github.io/bin/"
+    prefix = "https://github.com/leanprover/leanprover.github.io/raw/8fb36e926a3c4df8b84bfafedb7f39687f24b93b/bin/"
     if platform.architecture()[0] == "64bit":
         if platform.system() == "Linux":
             return prefix + "ninja-1.5.1-linux-x86_64"
$ sudo apt install python3 git libgmp-dev libmpfr-dev
$ git clone https://github.com/leanprover/lean2.git
$ cd lean2
$ patch -p1 < path/to/linja.patch
$ mkdir -p build/release
$ cd build/release
$ cmake -DCMAKE_BUILD_TYPE=Release ../../src
$ make -j4 install DESTDIR=.

上の例ではDESTDIR=.を指定することで./usr/localにインストールしているが、これを外せば/usr/localにインストールされる。

検証条件に対するLEAN2の実行

lean2にはlean3のような--makeオプションがついていない。以下のようなMakefilethysの直下に置くとよい。(LEANDIRを適切に変更する)

#!/usr/bin/make -f

LEANDIR = /somewhere/lean2/build/release/usr/local
LEAN = $(LEANDIR)/bin/lean

LEAN_SOURCES = $(shell find . -name '*.lean')
LEAN_BINARIES = $(LEAN_SOURCES:.lean=.olean)
LEAN_DEPFILES = $(LEAN_SOURCES:.lean=.d)

all:
  $(MAKE) deps
  $(MAKE) all2

deps: $(LEAN_DEPFILES)

all2: $(LEAN_BINARIES)

clean:
  $(RM) $(LEAN_DEPFILES) $(LEAN_BINARIES)

.PHONY: all deps all2 clean

%.d: %.lean
  (echo $<:; $(LEAN) --deps $<) | tr '\n' ' ' > $@

%.olean: %.lean
  $(LEAN) $< -o $@

-include $(LEAN_DEPFILES)

これを配置した上で thys 直下で make を実行すると、証明がコンパイルされる。

まとめと感想

Electrolysisの機能を一通り動かすことができた。

実は別のRustバージョンや別のLeanバージョンで動かせないか検討したがかなり困難であることがわかった。

Rustの検証プロジェクトではむしろRustBeltが有名で、メンバーから考えてもかなり期待が持てる。RustBeltとElectrolysisは以下のように異なる。

  • 検証の目的: RustBeltはunsafeな動作を含むより低レベルな操作に対し、UBを踏まないなどの証明をターゲットにしている。Electrolysisはより高級な変換で、アルゴリズムの正当性や計算量の検証を目指している。
  • ロジック: RustBeltは高階並行分離論理フレームワークIrisに立脚している。
  • 証明支援系: RustBeltはCoqで検証する。ElectrolysisはLeanで検証する。
  • 検証条件の抽出: Electrolysisは実際のRustコード(MIR)からの抽出に対応している。RustBeltは今のところMIRからの抽出には対応していない(Coq側の対応するコードは手動で書かれている)が、Ralf Jung氏が最近MIRの改造に取り組んでいるところから見るに、そのうち対応すると思われる。

Rust組込みトレイトのコヒーレンス

以下のトレイトは通常のコヒーレンス規則に加えて、特別なコヒーレンス規則が適用される。

Sized, Unsize

Sized, Unsize の手動実装を与えることはできない

Fn, FnMut, FnOnce

Fn, FnMut, FnOnce の手動実装は安定版では禁止されており、 #![feature(unboxed_closures)] が必要である

Drop

Dropはユーザー定義の構造体・列挙型・共用体にのみ定義できる。

また、(なぜかコヒーレンスチェッカーではなくDropチェッカーの一部になっているが)Drop は元の構造体・列挙型・共用体のジェネリクスを特殊化してはならない。これにより Drop は、各ADT型に対して定義されるか、定義されないかのどちらかになる。

Copy

Copy の実装は以下の条件を満たしている必要がある。

  • Self はユーザー定義の構造体・列挙型・共用体である。
  • その impl に課された境界から、各フィールドが Copy であることを結論づけられる。
  • この構造体・列挙型・共用体は Drop を実装していない。

CoerceUnsized

CoerceUnsized の実装は以下の条件を満たしている必要がある。

  • 両辺ともポインタ/参照型であるか、両辺とも構造体である。
  • ポインタ/参照型の場合、 (これは libcore で網羅されている)
    • ポインタからポインタ、ポインタから参照、参照から参照のいずれかである必要がある。
    • mut から mut, mut から const, const から const のいずれかである必要がある。
    • 参照から参照への場合は、大きいリージョン(部分型づけの意味では小さい)から小さいリージョン(部分型づけの意味では大きい)への変換である必要がある。
  • 構造体の場合、
    • 両辺が同じ定義を指している必要がある。
    • 両辺のフィールドをそれぞれ単一化したとき、ちょうど1個だけが失敗する必要がある。
    • 単一化が失敗したフィールドに対して同様に CoerceUnsized が成り立っている必要がある。

Rustにおける再帰的/余再帰的なトレイト選択/トレイト履行

Rustでは以下のようなプログラムはコンパイルエラーになる。

struct List<X>(Option<Box<(X, List<X>)>>);

// 通常は X: Clone を仮定するが、あえて Option<Box<(X, List<X>)>>: Clone としてみる
impl<X> Clone for List<X> where Option<Box<(X, List<X>)>>: Clone {
    fn clone(&self) -> Self {
        List(self.0.clone())
    }
}

fn main() {
    let x = List::<i32>(None).clone();
}

このとき、 List<i32>: Clone をするために以下のような推論が行われる。

  • List<i32>: Clone は上で定義されている impl を使うことができる。
  • そのためには where 節にある Option<Box<(i32, List<i32>)>>: Clone を充足する必要がある。
  • これには impl<T: Clone> Clone for Option<T> を使うことができる。
  • そのためには where 節にある Box<(i32, List<i32>)>: Clone を充足する必要がある。
  • これには impl<T: Clone> Clone for Box<T> を使うことができる。
  • そのためには where 節にある (i32, List<i32>): Clone を充足する必要がある。
  • これには impl<T0: Clone, T1: Clone> Clone for (T0, T1) を使うことができる。
  • そのためには where 節にある i32: CloneList<i32>: Clone を充足する必要がある。
  • i32: Cloneimpl Clone for i32 を使うことができる。
  • List<i32>: Clone を解決する必要があるが、これは元の問題と全く同じであるため失敗とみなす。

むろんこれは、 Clone の実装の where 節に普通使わない書き方を採用したからであり、 X: Clone とすればこのような再帰的な解決は不要になる。

例外として、帰納的なマッチング (coinductive matching)が許されるケースがある。それは以下のケースである

  • 検出されたサイクル上に登場する全てのトレイトが既定実装を持つとき。

例えば、先ほどの例で出てきた List<i32>Send かどうかを調べようとすると、以下のような推論が行われる。

  • List<i32>: Send には他の候補はないため、既定実装候補が採用される。
  • List にはフィールドが一つあるため、 Option<Box<(i32, Lists<i32>)>>: Send を充足する必要がある。
  • Option<Box<(i32, Lists<i32>)>>: Send には他の候補はないため、既定実装候補が採用される。
  • Option にはフィールドが一つあるため、 Box<(i32, Lists<i32>)>: Send を充足する必要がある。
  • Box<(i32, Lists<i32>)>: Send には他の候補はないため、既定実装候補が採用される。
  • Box にはフィールドが一つあるため、 Unique<(i32, Lists<i32>)>: Send を充足する必要がある。
  • Unique<(i32, Lists<i32>)>: Sendimpl<T: Send + ?Sized> Send for Unique<T> を使うことができる。
  • そのためには where 節にある (i32, Lists<i32>): Send を充足する必要がある。
  • (i32, Lists<i32>): Send には他の候補はないため、既定実装候補が採用される。
  • (_, _) にはフィールドが二つあるため、 i32: SendLists<i32>: Send を充足する必要がある。
  • i32: Send には他の候補はないため、既定実装候補が採用され、条件なしで充足される。
  • Lists<i32>: Send を解決する必要があるが、これは元の問題と全く同じである。通常ならばこれは失敗となるが、余帰納的なマッチングの条件を満たしているため、その場で成功とみなす。

なお、Rust 1.19.0時点では、この制約はトレイト履行(fulfillment)の場合にのみ適用され、トレイト選択(selection)時には余帰納的かどうかに関わらず再帰的なマッチングは認められていた。現時点での最新版では、#42840一部として、同じ制約がトレイト選択でも使われるようになっている。そのため、stableとnightlyでは以下のように表示されるエラーが異なっている。

stable

error[E0275]: overflow evaluating the requirement `List<i32>: std::clone::Clone`
  --> src/main.rs:11:31
   |
11 |     let x = List::<i32>(None).clone();
   |                               ^^^^^

nightly

error[E0599]: no method named `clone` found for type `List<i32>` in the current scope
  --> src/main.rs:11:31
   |
11 |     let x = List::<i32>(None).clone();
   |                               ^^^^^
   |
   = note: the method `clone` exists but the following trait bounds were not satisfied:
           `std::option::Option<std::boxed::Box<(i32, List<i32>)>> : std::clone::Clone`
   = help: items from traits can only be used if the trait is implemented and in scope
   = note: the following trait defines an item `clone`, perhaps you need to implement it:
           candidate #1: `std::clone::Clone`