如何將ML中的兩個數字劃分爲數據類型？

Question

我試着寫在SML接收兩個自然數N1，N2遞歸函數，並返回N1 N2 DIV的結果

數據類型自然被定義如下：

datatype natural = zero | Succ of natural 

我想按照新的數據類型來寫它，或者換句話說，不要將它們轉換爲常規形式並將結果轉換回來。

任何想法在這個定義中如何劃分？

Answer 1

你可以通過定義減法開始：

exception Negative 

fun sub (a, zero) = a 
    | sub (zero, b) = raise Negative 
    | sub (Succ a, Succ b) = sub (a, b) 

從這裏，應該是很容易簡單地指望有多少次，你可以從n1減去n2沒有去否定。特別是，這個公式應該有所幫助：

n1 div n2 = 1 + (n1 - n2) div n2 

我會把剩下的給你。

Answer 2

山姆Westrick的定義類似，「次數可以從n1減去n2沒有去否定」，你也可以做整數除法用加法和大於使用的定義，「次數可以添加n2到本身之前它大於n1「。

datatype nat = Z | S of nat 

fun gt (S x, S y) = gt (x, y) 
    | gt (S _, Z) = true 
    | gt (Z, _) = false 

fun add (x, Z) = x 
    | add (x, S y) = add (S x, y) 

fun divide (_, Z) = raise Domain 
    | divide (x, y) = (* ... *) 

加法似乎比減法在概念上更簡單。但是，更重要的是，比確定數字是否爲負數更昂貴的操作員，因爲這種情況是由歸納引起的，所以Sam的建議會更有效。

你可能會與下面的測試測試您的解決方案：

fun int2nat 0 = Z 
    | int2nat n = S (int2nat (n-1)) 

fun nat2int Z = 0 
    | nat2int (S n) = 1 + nat2int n 

fun range (x, y) f = List.tabulate (y - x + 1, fn i => f (i + x)) 

fun divide_test() = 
    let fun showFailure (x, y, expected, actual) = 
      Int.toString x^" div "^Int.toString y^" = "^
      Int.toString expected^", but divide returns "^
      Int.toString actual 
    in List.mapPartial (Option.map showFailure) (
     List.concat (
      range (0, 100) (fn x => 
      range (1, 100) (fn y => 
       let val expected = x div y 
        val actual = nat2int (divide (int2nat x, int2nat y)) 
       in if expected <> actual 
        then SOME (x, y, expected, actual) 
        else NONE 
       end)))) 
    end