私は次のいずれかが起こると考えて、ghciに次のように入力しました。1）インタプリタがハングし、述語に一致するものを無限リストのすべてのメンバーで検索します。または2）カーテンの後ろにあるハスケル柔術を通して、通訳はシーケンスが4で終了し、そこで停止することをどういうわけか理解します。
[x | x <- [1..],5>x]
結果1が起こった。さて、結果2は多くのことを求めていました。しかし、人間はシーケンスが4で終了することを証明できるので、インタプリタにそれを実行させる方法があるでしょうか？これは、終了するように書き直すことができますか？実際、無限のリストから有限の理解を生み出す述語はありますか？
しかし、人間はシーケンスが4で終了することを証明できるので、インタプリタにそれを実行させる方法があるでしょうか？
この単純なケースでは、そうです。>nしかし、Haskellはチューリング完全であるため、一部の自然数について式が真か偽かを判断する一般的なアルゴリズムは存在できませんn。したがって、式がすべての自然数の終了プログラムを表すことを証明することは不可能です。
式が基本的な整数演算に制限されている場合でも、一般的なケースでは、その真理は決定不可能です。
これは、終了するように書き直すことができますか？
モグがコメントで書いたように、それはtakeWhile (< 5) [1..]です。
takewhile上記のように、特定の問題に対する正しい解決策です。
ただし、これは、あなたの場合、すべての受け入れ可能な引数がすべての受け入れられない引数の前にあり、一般的なリスト内包がその制約に従わないためです。インタプリタにシンボリック推論を追加して、それ以上の要素が受け入れられないことを証明して終了できるようにすることは確かに可能です。（実際、Haskellの洗練された型システムはそのような推論を実装するのに非常に役立ちます。）しかし、検出器は評価されるすべてのリスト内包で[|]実行する必要があるため、これを標準演算子に追加することは意味がありません。非常に多くのコンピューティング費用を除いて、何も貢献できないことがよくあります。
「しかし、人間はシーケンスが4で終了することを証明できるので、インタプリタにそれを実行させる方法があるでしょうか？」
良い質問。難しいのは、4で終了するという証拠ではなく、4で終了する可能性があるという考えに続いて、これが実際にそうであるという洞察です。