データ型として定義されたML内の2つの数値をどのように分割できますか？

Question

私は、2つの自然数N1を受信SMLで再帰関数を記述しようとしてN2と、次のようにN1のdiv n2の

の結果を返すデータ型の自然が定義されています：

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 

私はあなたに残ります。サムWestrickの定義と同様に

Answer 2

、「あなたが負になることなく、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