問題タブ [non-termination]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
prolog - Prolog が正当な理由もなくローカル スタックから発生する
Prolog にレーベンシュタイン距離を実装しようとしています。
実装は非常に簡単です。
ただし、このコードは次のエラーで失敗します。
SWIPL
で実装を使用していMac OS X Sierra
ます。
isabelle - 非終結帰納述語
Isabelle / HOLの優れたプログラミングと証明では、次のように書かれています
[...] 再帰関数とは対照的に、帰納的定義には終了要件はありません。(pdf p.40)
- これは、無限に深い派生ツリーを持つことが可能な帰納的定義があることを意味しますか?
- そのような非終了の派生 (できれば無限の高さを持つもの) の例は何ですか? これらをどのように「構築」しますか?
- これらの規則誘導の原則はどのようにまだ健全ですか?
prolog - ゴールの並べ替え後に Prolog が終了しない
私は現在、Learn Prolog Now の例に取り組んでいます。1 つの演習では、1 つのルールにわずかな変更を加えるだけで、ローカル スタックが不足する KB があります。これはKBです:
および関連するルール:
そして、これは問題のクエリであり、スタックを使い果たします:
しかし、ルールを次のように変更すると
その後、動作します。
クエリをトレースすると、次のようにすぐに行き詰まります。
しかし、理由がわかりません。ラグランがエンドステーションであり、1 レベル後戻りする必要があることを理解するだけでよいのではないでしょうか?
ありがとう!
編集:SWI Prologを使用しています
編集:段階的に問題を解決した後、問題を見つけました。ラグランの場合、どこにもルールはありません。したがって、 を試行した後、(最後のルールの最初のゴール) を再試行するため、ループしますbyPlane, byTrain, byCar
。travel(raglan, X)
しかし、他のルールがどのように優れているかはわかりません。
agda - Well-Founded 再帰は安全ですか?
終了を隠す条項付きの非終了に関する質問では、答えはに頼ることを示唆してい<-wellFounded
ます。
<-wellFounded
beforeの定義を見たところ、 --safe
inがあることに気づきましたOPTIONS
。このオプションなしで動作することを意図していますか? つまり、--safe
何らかの最適化を使用していますか、それとも根本的な問題を回避していますか? この場合、終了の問題を「安全」とマークされた関数に委任するだけですか?