代数データ型の代数をさらに乱用する - これはなぜ機能するのですか？

Question

私は、this SO questionとthis 3 part seriesとespecially thisのようなページで、ADTを実数に似ていて操作する方法を読んでいます。

最後のリンクの「トラブル」セクションが私の目を引っ張り、記事には不可能と書かれていても、Natを解決しようとしました。

Nat = 1 + Nat 
Nat - Nat = 1 
Nat(1 - 1) = 1 
Nat = 1/(1 - 1) 

私はちょうど0で割ったので、これは総ナンセンスのように見えるかもしれません（とあなたが正しいかもしれない）が、あなたはそれらのリンクまたは類似のもののいずれかを読めば、あなたはそれが非常に似ていることに気づくでしょうリストの定義。

List(x) = 1/(1 - x) 

だからあなたはあなたが開始式で繰り返し置換することにより得るでしょう正確に何である、Nat = List(1) = 1 + 1 + 1 + ...のようにNATを書くことができます。また、これはHaskellで、このような自然数の定義と同等です：自然数、0 = []とS(N) =() : Nの有効なエンコーディングは間違い

type Nat = [()] 

はどれ。

---

私の質問はどのように私はこれから有効な結果を得たのですか？私はちょうど0で割った。始動方程式自体はほとんど矛盾であることは言うまでもありません。

このように私は何の意味があるのでしょうか？これはちょうど純粋な偶然の一致ですか、あるいはこの文脈で何らかの形で定義された0による除算ですか？

Answer 1

Natは無限であるため、Nat - Nat = Nat ⋅ (1 - 1) = Nat ⋅ 0 = 0を実際に使用することはできません。差Nat - Natは、であり、有限個数であるのに対し、Natは明らかに無限である。したがって、1 - 1は実際にはゼロではありません。nonstandard analysisでは極端に小さい値のようです。あなたが無限小で何かを分けるならば、あなたは何かを大きく（無限大、確かに...まあ）得るが、あなたはちょうどゼロに分割することはできない。それが有限であれば、あなたはゼロ除算されるので -

は実際に、私はあなたがについて尋ねたというパラドックスが「Natが無限であることを証明」として見ることができると思います。

もちろん、あなたは実際にはそうではありませんこのタイプの算術演算は何でもあります...それは面白い娯楽ですが、実際には数学的ではありません。