問題タブ [combinators]

私はコンビネータ論理で定理を証明するいくつかの実験を行っていますが、これは有望に見えますが、つまずきのブロックが 1 つあります。コンビネータ論理では、たとえば I = SKK が真であることが指摘されていますが、これは定理ではありません。を公​​理として追加する必要があります。追加する必要がある公理の完全なリストを知っている人はいますか?

編集: もちろん、I = SKK を手で証明することはできますが、何かが欠けていない限り、それはコンビネータ ロジックと同等のシステム内の定理ではありません。そうは言っても、I を SKK にマクロ展開することはできますが、まだ何か重要なものが欠けています。通常の 1 階論理では矛盾を解決しやすい節 p(X) と ~p(X) の集合を SK に変換し、代入を実行して S と K のすべての呼び出しを評価すると、私のプログラムは以下（Unlambdaのバックティックに ' を使用しています）：

''eq''s''s''s'ks''s''s'ks''s'kk'keq'''s'ks'kk'kk''s'kk'k false 'k true 'k true

私が必要としているのは、部分呼び出し「k」と「」を処理するための適切な一連のルールのようです。これらのルールがどうあるべきかわかりません。この分野で見つけることができるすべての文献は、プログラマーではなく、数学者を対象としています。理解すれば、答えはおそらく非常に簡単だと思います。

キーワードを使って単語の繰り返しを終わらせる方法を見つけようとしています。例：

実行すると

を出力し、パーサーが入力内のキーワードを消費したwords: List(one, two, END)ことを示し、式パーサーが一致できなくなります。と一致しないようにしたいと思います。これにより、正常に解析できるようになります。wordsENDENDwordsexpression

誰がどのように機能するか説明できますfoldrか?

次の例を見てください。

私はこれらの処刑について混乱しています。助言がありますか？

最近私を悩ませている簡単な質問。Haskellは、偽の値を返したとしても、ブール値を返す関数ですべての等価性テストを実行しますか？

例えば

最初のテストがfalseを返した場合、？の後に2番目のテストを実行し&&ますか？それとも、Haskellはそれをせずに先に進むのに十分怠惰ですか？

タイプのバイナリコンビネータが必要です

または多分

（これは最初のfoldr1にすぎませんが、通常は2つのブール関数を組み合わせるだけで済みます。）

これらは組み込みですか？

そうでない場合、実装は簡単です。

多分

Hoogleは何も表示しませんが、検索が適切に一般化されない場合があります。これらが組み込まれているかどうかはわかりますか？それらは既存のライブラリの断片から構築できますか？

これらが組み込まれていない場合は、これらの名前がかなり悪いため、新しい名前を提案する可能性があります。実際、それが私がそれらが組み込まれていることを望む主な理由です。

タプルにいくつかの量を追加したいと思います。それを取り出して合計して見せたいです。Foldr機能を使いたい。

誰かが私にやり方を手伝ってくれる？

次のエラー メッセージが表示されます。

コンビネーターパーサーで表現されたあいまいな言語があるとします。特定の式をローカルで貪欲にする方法はありますか? これが私の言いたいことの例です。

コンパイル後、次のように実行できます。

の最初の部分をobjローカルに貪欲にして と一致するように何らかの方法で指示したいと思いlongchainます。順序を入れ替えると に一致しますが、それlongchainは欲張りのせいではありません。

高階コンビネータ（または関数プロデューサー）は、連結および暗黙のプログラミングでどのような正確な役割を果たしますか？

スタックを直接操作するのではなく、連結プログラミング言語を実装する別の方法はありますか？

言及されたコンビネータとSchonfinkelのコンビネータ論理の間の関係はどのくらい緊密ですか？

この質問の myAny 関数のコードでは、foldr を使用しています。述語が満たされると、無限リストの処理を停止します。

私はfoldlを使ってそれを書き直しました：

(ステップ関数への引数が正しく逆になっていることに注意してください。)

ただし、無限リストの処理が停止することはなくなりました。

Apocalispの回答のように、関数の実行を追跡しようとしました:

ただし、これは関数の動作方法ではありません。これはどのように間違っていますか？