for-times

たぶん『計算可能性・計算の複雑さ入門』.icon固有の名詞

whileに少し制限を加えたfor..times構文

for |n| times do stmt end-for

任意のループはwhileだけで表現可能だが、そこで敢えて制限のあるfor-timesに着目することで、「計算がいつ終わるからない」性質がアルゴリズム記述のための本質であることを見出す

任意のデータを計算の基本要素に変換するときに関数を作ってたが、

それらの関数は全部for-timesで記述可能

なのでfor-timesがあれば$ \Sigma^\star上で任意のデータ型を表現可能

つまりfor-timesは計算の基本要素より抽象的でprimitiveだということ #??

まじ？

任意の単純for-timesプログラムは必ず停止する

単純for-timesプログラム

以下のみで構成されるプログラム

データ型:$ \Sigma^*

$ \Sigma^*は文字列型の$ \{0,1\}

演算: 文字列上の基本演算

実行文: 代入、if, for-times, halt

ref 計算の基本要素

for-timesの代わりに拡張for-timesを使ってもほぼ同じ

for <パラメータ> times do <文;..;文;> end-for

パラメータの部分は回数を表す変数

for-times計算可能

関数$ fを計算する単純for-timesプログラムが存在するとき、「$ fはfor-times計算可能」であるという

帰納的関数論の原始帰納に対応する

繰り返しに明らかな上限がある

これはwhile文よりかなり強い条件

これにより、for-times文は任意の入力に対し、必ず停止する

for-times計算可能な関数の例

pair

タプル系

1st

2nd

配列系

create

get

put

計算可能な関数は全てfor-times計算可能かどうか

否

for-times計算可能でないものの例

giant

code:hs

giant x = foldl (^) x $ replicate (x-1) x

giantはxをxにx回冪乗する

ex. giant 3 = 3^3^3

ex. giant 4 = 4^4^4^4

giantは計算可能であるがfor-times計算可能ではない

つまり、whileとfor-timesの差が現れている

みすってるかもmrsekut.icon*3

loong

code:hs

loong x = replicate (giant x) 0

つまりlength $ loong xが giant xと一致する

loongがfor-times計算不可能であることを証明する

参考

『計算可能性・計算の複雑さ入門』