[過去ﾛｸﾞ]
次世代言語11[Rust Swift TypeScript Dart] (1002ﾚｽ)
次世代言語11[Rust Swift TypeScript Dart] http://mevius.5ch.net/test/read.cgi/tech/1528037607/
上
下
前次
1-
新
通常表示
512ﾊﾞｲﾄ分割
ﾚｽ栞
抽出解除
ﾚｽ栞
このｽﾚｯﾄﾞは過去ﾛｸﾞ倉庫に格納されています｡
次ｽﾚ検索
歴削→次ｽﾚ
栞削→次ｽﾚ
過去ﾛｸﾞﾒﾆｭｰ
578: デフォルトの名無しさん [] 2018/06/18(月) 15:30:15.87 ID:soq2obRK ところで、またATS2に話を戻すんだけど、 日本語訳もあったしチュートリアルやってみてるんだけど ↓の再帰関数の停止性検査とやらで躓いている ttp://jats-ug.metasepi.org/doc/ATS2/INT2PROGINATS/x2485.html 特に fun isevn{n: nat} .<2*n>. (n: int n): bool = if n = 0 then true else isodd (n-1) and isodd{n: nat} .<2*n+1>. (n: int n): bool = not(isevn(n)) が何故.<2 * n>.と.<2 * n + 1>になるか理解できん… .<n>.と.<n + 1>.で大丈夫だと思ったんだが… たぶんまだ、停止性メトリクスとやらが正しく理解できていないんだろうな… 誰か詳しく解説してくれないか？ http://mevius.5ch.net/test/read.cgi/tech/1528037607/578
588: デフォルトの名無しさん [sage] 2018/06/18(月) 18:02:04.30 ID:EvkbZGBx >>578 isevn.<n>.とisodd.<n+1>.だと isevn 3 のメトリックは.<n>. = .<3>. そこから呼ばれるisodd 2 のメトリックも.<n + 1> = .<3>. 減ってねえ！エラー！ってことじゃね 想像だけで試してないので違ってたらすまん http://mevius.5ch.net/test/read.cgi/tech/1528037607/588
589: デフォルトの名無しさん [sage] 2018/06/18(月) 18:04:53.53 ID:xdRdwSco >>578 とある関数呼び出しの定義内に表れる再帰的呼び出しの 停止性マトリクスが、大元の関数呼び出しの停止性マトリクスから辞書順で下降していくことから停止性を担保しようというのが停止性マトリクスの意味。 そして停止性マトリクスの記述に表れる n は issven や isodd の引数そのものだということに注意 iseven、isodd の停止性マトリクスがそれぞれ n、n+1 だと、 iseven n の停止性マトリクス→n iseven n の定義に出てくる isodd (n-1) の停止性マトリクス→n-1+1=n 減っていないから停止性が担保されない(NG)。 説明にあるように <n, 0> と <n,1> ならば、 iseven n の停止性マトリクス→<n,0> iseven n の定義に出てくる isodd (n-1) の停止性マトリクス→<n-1,1> (下降している！OK) isodd も同様に isodd n の停止性マトリクス→<n,1> isodd n の定義に出てくる iseven (n) の停止性マトリクス→<n,1> (下降している！OK) そして<n,0>, <n,1> の代わりに n*2, n*2+1 を使っている(この代用が可能なことはわかるよね)。 http://mevius.5ch.net/test/read.cgi/tech/1528037607/589
ﾒﾓ帳
(0/65535文字)
上
下
前次
1-
新
書
関
写
板
覧
索
設
栞
歴
ｽﾚ情報
赤ﾚｽ抽出
画像ﾚｽ抽出
歴の未読ｽﾚ
AAｻﾑﾈｲﾙ
Google検索
Wikipedia
ぬこの手
ぬこTOP
0.167s*