問題タブ [church-encoding]

N正の整数の Church エンコーディングでは、再帰原理を定義できnat_recます。

次の教会の平等のequal_recコード化の再帰原則は何ですか?equal

次のコードでは、ステートメントadd'_commutは Coq によって受け入れられadd_commutますが、ユニバースの不一致のために拒否されます。

どうすれば通り抜ける？

タイプチェッカーおよびエバリュエーターとして Agda を使用して、システム F でいくつかの定義をテストしたいと思います。

教会の自然数を紹介する私の最初の試みは、次のように書くことでした

これは、通常のタイプ エイリアスと同じように使用されます。

ただし、 の定義はNum型 (種類?) チェックを行いません。それを機能させ、システム F 記法にできるだけ近づけるための最も適切な方法は何ですか?

私は関数型プログラミングと F# の初心者です。演習として、教会の数字を実装しようとしています。
まず、数字を次のようにコーディングしました。

次に、数値が機能するかどうかを確認するヘルパー関数を作成しました。

例えば：

予想どおり、3を出力します。
また、いくつかの算術関数を実装しました。

それらはすべて正常に動作しているようです:

しかし、私は減算を実装するのに本当に苦労しています:

上記の方法は、減算ではなくある種の指数のように見えます。
私も試しました（wikiが示唆するように）：

しかし、使用しようとすると型の不一致が発生します:

私は立ち往生しています、私は何を間違っていますか? また、コードを改善するための提案もいただければ幸いです。

フリーライブラリのFreeT型を使用して、基になる を「実行」するこの関数を記述しています。StateT

ただし、代わりに、教会でエンコードされたバージョンであるFTで動作するように変換しようとしています。

しかし、私はまったく同じ運を持っていません。私が得たあらゆる種類の組み合わせは、うまくいかないようです。私が得た最も近いのは

しかし、最初の穴m r -> StateT s m rの型は であり、2 番目の穴の型はStateT s m r -> m r...つまり、その過程で状態を失うことになります。

FreeTすべての関数が で記述できることを知っていFTます。ラウンドトリップを伴わないFreeT(つまり、 と を明示的に一致させる必要がある方法でPure)これを記述する良い方法はありFreeますか? s(手動でインライン化を試みましたが、 の定義で異なる を使用して再帰を処理する方法がわかりませんrunStateFree)。それとも、これは、明示的な再帰データ型が教会 (mu) エンコーディングよりも必然的にパフォーマンスが高いケースの 1 つですか?

教会の数字の後継者と前身者の次のコードがあります。次のコードを検討してください。

pred 関数で次の変更を行うとします。

x と (x) を返すことの違いは何ですか? (x) を返すことは、構文的および論理的に正確に何を意味しますか?