如何将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