アカウント名:
パスワード:
多分, 有名な停止問題 [nagoya-u.ac.jp]を知らないんでしょう.
より多くのコメントがこの議論にあるかもしれませんが、JavaScriptが有効ではない環境を使用している場合、クラシックなコメントシステム(D1)に設定を変更する必要があります。
普通のやつらの下を行け -- バッドノウハウ専門家
あるなら俺にくれぃ! (スコア:3, おもしろおかしい)
1を聞いて0を知れ!
Re: (スコア:0)
Re: (スコア:0)
Re: (スコア:2, 参考になる)
多分, 有名な停止問題 [nagoya-u.ac.jp]を知らないんでしょう.
Re:あるなら俺にくれぃ! (スコア:0)
Re:あるなら俺にくれぃ! (スコア:1)
一応マジレスしておくと,言語にチューリングマシンと同等の記述能力を持たせようとすると,そもそもあるプログラムに無限ループ構造があるかを判定するのが無理(停止するかどうかを判定するのに無限の時間がかかる)というのが停止問題のおおざっぱな内容.ちなみに,プログラミング言語にはチューリングマシンと同等の記述能力を持たせるのが普通じゃないかなぁ(ここは自信なし).
Re: (スコア:0)
っていう前提が停止問題での無限ループを判定するのは無理という話ですよね。
つまり、チューリングマシンを前提としている。
すでに純粋関数型言語ではチューリングマシンの前提の一部は崩れている。
有限のリストを実用上必要とするときに無限ループを組むことはあるが、
それは言語仕様の本質とはずれている。
純粋関数型言語をもう少し進化させると、状態変化を伴う無限ループを記述すること自体できないような仕様の進化があり得ないとまでは言えない。
とすれば、無限ループを評価できないのは言語仕様に依存すると言えるでしょう。
Re: (スコア:0)
これは初耳です。もう少し詳しく説明してください。
Re: (スコア:0)
・順次評価
・ループさせながら状態を変化させて解を探索
を持っていない
評価されなければ無限ループには陥らない。
たとえば、循環参照を定義したとしても、それをプリントするまでは無限ループしない。(CやJavaのようなチューリングマシンも)
逆にプリントという副作用を定義するときは有限の限界値を指定しない限り実行できないという仕様にする。
(普通はプログラマが自主的にケアしてしまえば済むなので実用性がないだけ。言語仕様として実装は可能)
# 停止性問題は非決定性チューリングマシンに対してまでは証明されているんだろうか?
Re: (スコア:0)
# 非決定性も決定性でシミュレートできますよ。
Re: (スコア:0)
関数型言語の入門部分をラムダ関数で表現できたからといって、
結局同じと言ってしまうあたり、言語仕様の理解、大丈夫です?
仮に完全にエミュレートできたとしてもそれはチューリングマシンで
関数型言語の仕様を実現するのであって、
その時にはチューリングマシンの持っている特性の一部は関数型言語の仕様の名のもとに制約を受ける。
よってチューリングマシンでの命題が関数型言語でも同値とは言えないよね
Re: (スコア:0)
Re: (スコア:0)
その部分は純粋関数型言語とは逸脱する純粋じゃない部分。
純粋じゃない関数型言語ならチューリングを実装できるでしょう。
# てか最初から純粋関数型言語の仕様をさらに進化させればと書いているけど
関数型言語で副作用を実装するための工夫は各言語の実装依存だけれど、
あえて、その副作用を言語仕様に持ち込むときに、
・有限のステップであることが分かっている型(関数)だけを順次評価(状態変化順を許容)する。
・未知の部分は評価せず、定義のみを返すような言語仕様にする。
(未知のものを停止するかどうかを完全に証明するのは無理というのが停止性問題という理解で正しければ)
そのような言語仕様をたてれば、任意の関数が有限のステップで終了するかどうかを証明する必要はないそもそもない
(有限ステップで評価可能とわかっているものしか評価しないので。)
Re: (スコア:0)
# 有限ステップ云々は #1367998 の言う PS vs PDF のようなイメージでしょうか。
# 再帰関数が定義できなかったりする?
Re: (スコア:0)
副作用の話はTMと純粋関数型言語の根本的な違いですので、必要と思いました。
> 純粋関数型で TM は実装できると思いますよ。
知ってるなら話は早いです。
関数型言語でTMを実装したことあります?
評価順を指定できるような非純粋仕様部分で実装しますよね。(たとえばモナドとか)
そこに制約を与えるような言語仕様を作れば目的は達せられるという話。
> # 有限ステップ云々は #1367998 の言う PS vs PDF のようなイメージでしょうか。
違います。
言語仕様としての値の評価順の問題で、異常停止させずに正しい参照を返せます。
> # 再帰関数が定義できなかったりする?
できます。
しかしチューリングマシンのように順次評価ではないので、再帰関数でも無限ループしません。
# 純粋関数型言語が存在する意義はそこにある。
Re: (スコア:0)
モナドとか使わずに、普通の関数でも実装できますよ。
(それにすべてのモナドが副作用を伴うわけでもないし)
> しかしチューリングマシンのように順次評価ではないので、再帰関数でも無限ループしません。
例えば Haskell のような言語だと、
let ones = 1:ones in last ones
のような例で停止しないです。
Re: (スコア:0)
関数型などを進化させた仕様って書いてます。
コンパイル時にcheck-termination機能がある純粋関数型言語はあるわけで、それを洗練させて、有限で処理できるものだけを評価すればいいという「仕様」の問題だという命題は全然否定されないんですけど。
そのlet in で、check-terminationを通るとでも?
Re: (スコア:0)
Re: (スコア:0)
チェックを通らない部分については関数への参照のまま返される。
チェッカーを改善していくことで、その確率を限りなく減らして実用性を引き上げる。
(0にはならなくても)
Re: (スコア:0)
実用的な意味ではインタプリタの類いは全く書けなくなってしまうので、
それをプログラミング言語と呼ぶのは抵抗があるなあ。
# でもようやくあなたの主張がわかりました。
# さっきのonesの例はコラッツの問題でも使えばよかったのかな。
Re: (スコア:0)
それが理論上無限でも遭遇しなければいいっていうのが実用性で
> 実用的な意味ではインタプリタの類いは全く書けなくなってしまうので、
インタプリタが書けないということもないし、インタプリタが書けるかどうかと言語の必須要件ではまったくないわけで。
↓そうですか、としか言えない。
> それをプログラミング言語と呼ぶのは抵抗があるなあ。
# ex . Agda2はまだ実用性はないのかもしれないが、立派なプログラミング言語だと思うけどなぁ・・・
Re: (スコア:0)
> その通り。私が言っている仕様なら、不滅の力 マジンガーZ
> その通り。私が言っている仕様なら、人の頭脳を加えたときに
> その通り。私が言っている仕様なら、マジンガーZ!
> その通り。私が言っている仕様なら、マジンガーZ!
> その通り。私が言っている仕様なら、お前こそ勇気もたらす
Re: (スコア:0)
http://www.tcs.informatik.uni-muenchen.de/~abel/foetus/ [uni-muenchen.de]
AdgaはHaskellとかfoetusを利用してるね
Re: (スコア:0)
Re: (スコア:0)
Re: (スコア:0)
違います。チューリングマシンをエミュレートできる機械すべてが該当します。
チューリングマシンをエミュレートできないよう言語仕様に制約を加えることは可能かもしれませんが、それはチューリングマシンで解ける問題の一部が解けなくなると言うことです。