ghciに次の2つの事柄が発生すると考えて、以下のようにタイプしました。1）インタプリタが無限リストのすべてのメンバーを検索して述語に一致するかどうかを調べます。または2）カーテンの後ろを通ってHaskell jujitsuを通して、通訳者は何とかシーケンスが4で終了しそこで止まることを理解するだろう。無限リストの有限の理解
[x | x <- [1..],5>x]
結果1が発生しました。今、結果2は多くのことを求めていました。しかし、人間はシーケンスが4で終了することを証明することができるので、通訳者にそれをさせる方法があるだろうか？これは終了するように書き直すことができますか？実際には、無限リストの有限の理解をする述語がありますか？
しかし人間はシーケンスが4で終了することを証明できるので、通訳者にそれをさせる方法があるのだろうか？
この単純なケースでは、はいです。しかし、Haskellはチューリングが完了しているため、すべての自然数が>nの場合は真であるか偽であるかを判断する一般的なアルゴリズムは存在しないので、式がすべての自然数の終了プログラムであることを証明することはできません。
あなたの式が基本的な整数演算に限定されていても、その真実は一般的なケースではまだ決めることができません。
これは終了するように書き直すことができますか？
Mogがコメントに書いた通り、takeWhile (< 5) [1..]です。
は、だから、「それは更なる要素が許容できないと、その後終了することを証明することができるようにインタプリタに象徴的推論を追加することが可能であろう」という@Kilianに同意するでしょうか？ – gcbenison
@gcbenison：はい、いいえ。はい、可能かもしれません。いいえ、一般的なケースではうまくいかないため、通訳者は場合によっては正解のみを推測する*ことができます。言語を根本的に変えなければならないか、通訳者を定理証明者にするかのどちらかです。 –
@larsmans「通訳者を定理証明者に変える」というのは、とにかくそうすべきだからです。 ;） –
takewhileは、前述のように、特定の問題の正しい解決策です。
しかし、これは、受け入れ可能なすべての引数がすべての受け入れ不可能な引数の前に来て、一般的なリストの理解がその制約に従わないためです。通訳者に象徴的な推論を加えて、それ以上の要素が受け入れられずに終了することが証明されることは確かに可能です。実際には、Haskellの洗練された型システムは、そのような推論を実装するのに非常に役立ちます。しかし、これを標準の[|]演算子に追加するのは意味がありません。検出器はで実行する必要があります。リスト内包非常に多くのコンピューティング費用を除いて何かを寄付することができません。
これはUIの問題です。
Prologはcut演算子を持ちます。ハスケルでは、私たちが期待するソリューションの数を事前に指定することができます。あなたの複雑な例（コメント内）のように、take 5 $ map f [1..]は動作しますが、take 6 ...はまだループに入ります。それを克服するためには、定理証明者であるランタイムシステム（他の人が言っているように）、および/または時間認識マルチスレッドオプティミスティックの投機的な部分評価者が必要です各ユーザーの要求。これは、のタグ付け計算に優先順位値（また、言語レベルで）を伴うことになります。
これはすべて意味で非常にと考えています。とにかく、等式推論のアプローチの最初の約束であった直感的な簡単なコードを書くことができます。当初、コードは通常のHaskellモードで実行されますが、アナライザは遅延計算のために起動します。
通訳はとにかく、ほとんどの時間をアイドル状態にあります。ほとんどのコンピュータも。
（後添加）参照、例えば、the speculation packageから "安全な、プログラム可能な、投機的な並列のためのフレームワーク"。 「コンパイルされたコードを追加、コードの実行プロファイルの経験則に基づいて、実行時に動的に最適化された（および再最適化）された」
そしてもちろん、V8、。
「遅延計算」では、実行時間が長すぎる（壁時計の時間のように）完了したコードのアナライザーを実際に起動することを意味しますか？ – gcbenison
@gcbenisonそのようなもの。コンパイラも、今度は答えを出した後でさえ、バックグラウンドでもっと多くの作業を行うことができます*、より多くの最適化などを見つけることはもちろんです。それはもちろんすべての仮説です。 –
これは質問の答えよりも議論のポイントだと思います。そのような議論をするのに最適な場所ではありません。 –
"人間はシーケンスが4で終了することを証明できるので、 には通訳者にそれをさせる方法があるのでしょうか？"
難しいことは、それが4で終了するという証拠ではなく、4で終了する可能性があるという考え、それが本当にそうであるという洞察に続いています。
'takeWhile（<5）[1 ..]' – m09
@Mog：私はあなたのコメントにあなたに同意しながらあなたがやや理解の意味を変更したので、浮気されていませんか？プログラムについて何かを証明するために、人間の –
機能は常に自動プログラムを模倣することができるものではありません：あなたは、いくつかの特定のプログラムを終了できることを推論することができるかもしれないが、一般的に、これは（それは停止問題だ計算することはできません、決めることはできません）。そして、あなたはリストの理解に必要な任意のコードを書くことができます、私は一般的なケースでは、コンパイラはあなたのリスト内包について非常に困難な時間推論を持っていると考えています。 – gfour