如何划分定义为数据类型的 ML 中的两个数字？

Question

我正在尝试用 SML 编写一个递归函数，它接收两个自然数 n1、n2 和 returns n1 div n2

的结果

自然数据类型定义如下：

datatype natural = zero | Succ of natural

我想根据新的数据类型来编写它，或者换句话说，不是通过将它们转换为它们的常规形式然后再转换回结果。

知道如何在此定义中完成 division 吗？

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

类似于 Sam Westrick 的定义 "number of times you can subtract n2 from n1 without going negative"，您也可以使用定义 "number of times you can add n2 to itself before it is greater than 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

如何划分定义为数据类型的 ML 中的两个数字？

How can I divide two numbers in ML defined as a datatype?

sml

ml