問題タブ [peano-numbers]

Steve Yegge のポッドキャスト (#29、21:29 頃) を聞いていて、その中で「話している相手が賢いかどうかを見分ける方法」について話していました。 「ピアノの数字」や「ラムダ計算」などの「賢い人々のこと」（私は言い換えています）について話すことでした。
私は世界で最も賢い人ではないことを認めるのに十分安全ですが、Googleでさえ「ピアノ番号」が何であるかを教えてくれないようです. それで、ポッドキャストで言われたことを聞き間違えましたか? 「ピアノ番号」とは誰か教えてもらえますか？

私は関数を書こうとしています

整数をペアノ番号に変換します。

私はデータを持っています：

例えば、

等々。

整数を指定して Peano Numbers を出力する方法がわかりません。私はペアノ数を扱ったことがないので、これに関する助けがあれば大歓迎です!

ありがとうございました！

これは、ほぼ 2 年前に私が尋ねた質問のフォローアップです。ベクトル/行列/テンソルの次元が型システム (Peano 番号付け) を使用してエンコードされる小さな線形代数ライブラリを作成するために、型システムをまだ試しています。これにより、コンパイラは二項演算を対応する次元のオブジェクトに制限できます。

うまく機能しますが、各ディメンション タイプを手動で指定する必要があります。例（形のない自然数を使用）：

小さいサイズは問題ありませんが、サイズを定義する必要があると退屈になります_1024。(コンパイル時に) 整数リテラルを対応する Peano-number 型に変換する方法を見つけようとしています (成功せずに)。

Daniel Sobral の回答コメントで、Scala は依存型をサポートしていないため、これは不可能であると言われました。現在、Scala 2.10 には依存型とマクロの両方があります。それを達成する方法はありますか？

私は、ZFC 集合論、特にコンピュータ プログラムが無限公理をモデル化して自然数を「構築」する方法をよりよく理解しようとしています。自然数を構成するために使用される典型的な記号は、「{」、「}」、および「,」です。

以下のコードは機能しますが、純粋に再帰的なソリューションを望んでいます。自然数 (ここでは int を使用) を指定すると、対応する文字列を集合論的エンコーディングに再帰的に構築し、それを返します。理想的には、現在使用されている String 配列のような余分なデータ構造を使用せずに機能することを願っています。

ランタイムが遅い (指数関数的) 場合は問題ありません。再帰を使用すると、プロセスの表現がより単純で、より凝縮/エレガントになり、理解しやすくなることがあります。パフォーマンスに関係なく、このような解決策がどのように見えるかを非常に知りたいです。最終的には、数学/数の基礎をよりよく理解したいと思います。たくさんの質問がありますが、これは始めるのに良い方法かもしれないと思いました. ありがとう！

私は Rust で Peano 数の簡単な実装を書きたかったのですが、どうにかして基本を機能させることができたようです。

しかし、他の人がどのように実装したかを調べることにしたとき、誰もそれを anenumではなくstructs and PhantomData( example 1 , example 2 ) で行うことを決定したことがわかりました。

私の実装に何か問題がありますか？これは、ZeroandSuccがenumバリアントであり、真の型ではないためですか (したがって、私の実装は実際の型演算ではありません)? それとも、実装を拡張した場合に発生する問題のために、これを「主流」の方法で行うことが望ましいですか?

編集: sを使用してペアノ数を実装する際の私の苦労は、ここstructで見ることができます。