たぶん固有の名詞

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

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

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

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

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

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

まじ？

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

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

データ型:\Sigma^*

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

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

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

ref 計算の基本要素

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

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

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

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

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

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

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

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

pair

タプル系

1st

2nd

配列系

create

get

put

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

否

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

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

ex. giant 3 = 3^3^3

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

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

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

みすってるかも

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

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

参考