問題タブ [church-encoding]

私はソフトウェア基盤に取り組んでおり、現在は教会の数字に関する演習を行っています. 自然数の型シグネチャは次のとおりです。

succtypeの関数を定義しましたnat -> nat。次のように加算関数を定義したいと思います。

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

このエラー メッセージの実際の意味は何ですか?

ウィキペディアの定義に従って、教会の数字のゼロと教会の数字に関するその他の標準関数を次のように定義しました。

これらを使用して、再帰ループを次のように記述します。

上記の引数の場合、これは再帰に入ることなく をn0返す必要があります。n0しかし、そうではありません。なんで？

注 1: この再帰ループは、通常の数値と通常の関数で完全に正常に機能します。

これは正常に戻ります0。

注 2: 関数ifthenelse、iszero、newtrue、newfalseも単独で正常に動作します。

javascript で ES6 アロー関数を使用して、Church エンコーディングと Y-Combinator を実装することができました。しかし、階乗関数を評価しようとすると、

「Uncaught RangeError: Maximum call stack size exceeded(…)」エラーが発生しました。

FactGenを変更すると、

それだけで機能します。

私が知りたいのは、それの教会数字バージョンです。どうすればこれを達成できますか？

Haskell のポリモーフィック ラムダ計算でペアの Church エンコーディングを実装したいと考えています。

Peter Selinger のラムダ計算に関するノートの77 ページ、セクション 8.3.3 で、彼は 2 つのタイプのデカルト積の構成を次のように示しています。

A×B = ∀α.(A→B→α)→α<br/> ⟨M,N⟩ = Λα.λf ^A→B→α.fMN</sup>

別の情報源については、 Dider Rémy のラムダ計算に関するノートの54 ページ、セクション 4.2.3 で、彼は、多相 λ 計算/システム F でのペアのチャーチ エンコーディングを次のように定義しています。

Λα₁.Λα₂.λx₁∶α₁.λx₂∶α₂.Λβ.λy∶α₁→α₂→β. y x₁ x₂</p>

レミーはセリンジャーと同じことをもっと冗長に言っていると思います。

とにかく、ウィキペディアによると、Haskell の型システムはSystem Fに基づいているため、この Church エンコーディングを Haskell で直接実装できることを願っています。私が持っている：

しかし、私は予測を行う方法がわかりませんでした。

Λα.Λβ.λp ^α×β .pα(λx ^α .λy ^β .x)

forall大文字のラムダ型量指定子に Haskell を使用する必要がありますか?

これは基本的に前の質問と同じですが、Swift ではなく Haskell です。追加のコンテキストと会場の変更により、より賢明になる可能性があると思いました。

コメンテーターは最近次のように述べました。

無料のモナドは教会の数字です -- 関数の代わりに (endo-) ファンクタを使っているだけです!

彼は続けてこのことわざを次のように説明しています。

それらは両方とも 0 - n 回構成された endfunction(ion|or) です

Church Numerals は、数値ごとに 1 つの構成を持つ無名関数構成のセットであることがわかります。それがFree Monadsにどのように適用されるのかわかりません。

私の質問は: Free モナドは教会の数字ですか?

ラムダ式:λx.λy.x(xy)があり、その整数表現を推測することになっています。特に教会のエンコーディングと教会の数字についてたくさん読んだことがありますが、何の数字かわかりません。3 歳児が理解できるように説明してもらえますか、またはウィキペディアよりも優れたリソースを紹介してもらえますか?

Haskell について学び始めたばかりで、Haskell でラムダ計算を使用しようとしています。教会の数字を数値に変換するこの式を見つけましたが、この式の 0 が何を意味するのかわかりません。どこにも見つかりません：

私を混乱させるのは最後のゼロです。それはこのラムダ式の基本ケースですか、それともいくつかの引数ですか?