伊德里斯Gcd的总体定义

2 回答

• 0

  我有一个使用 Accessible 关系的版本，表明你找到gcd的两个数字的总和在每次递归调用时都会变小：https://gist.github.com/edwinb/1907723fbcfce2fde43a380b1faa3d2c#file-gcd-idr-L25

  它依赖于此，来自 Prelude.Wellfounded ：

  data Accessible : (rel : a -> a -> Type) -> (x : a) -> Type where
       Access : (rec : (y : a) -> rel y x -> Accessible rel y) ->
                Accessible rel x
  

  一般的想法是，您可以通过明确说明变小的内容来进行递归调用，并在每个递归调用上提供它确实变得更小的证明 . 对于 gcd ，它看起来像这样（ gcdt 为自 gcd 以来的总版本在前奏中）：

  gcdt : Nat -> Nat -> Nat
  gcdt m n with (sizeAccessible (m + n))
    gcdt m Z | acc = m
    gcdt Z n | acc = n
    gcdt (S m) (S n) | (Access rec)
       = if m > n
            then gcdt (minus m n) (S n) | rec _ (minusSmaller_1 _ _)
            else gcdt (S m) (minus n m) | rec _ (minusSmaller_2 _ _)
  

  sizeAccessible 在前奏中定义，并允许您在此明确声明's the sum of the inputs that'变小 . 递归调用小于输入，因为 rec 是 Access rec 的参数 .

  如果您想更详细地了解发生了什么，可以尝试用孔替换 minusSmaller_1 和 minusSmaller_2 调用，以查看您需要证明的内容：

  gcdt : Nat -> Nat -> Nat
  gcdt m n with (sizeAccessible (m + n))
    gcdt m Z | acc = m
    gcdt Z n | acc = n
    gcdt (S m) (S n) | (Access rec)
       = if m > n
            then gcdt (minus m n) (S n) | rec _ ?smaller1
            else gcdt (S m) (minus n m) | rec _ ?smaller2
  

  例如：

  *gcd> :t smaller1
    m : Nat
    n : Nat
    rec : (y : Nat) ->
          LTE (S y) (S (plus m (S n))) -> Accessible Smaller y
  --------------------------------------
  smaller1 : LTE (S (plus (minus m n) (S n))) (S (plus m (S n)))
  

  我不知道的任何地方，文件 Accessible 在很多细节，至少对伊德里斯（你可能会发现Coq的例子），但在 Data.List.Views 有更多的例子在 base 库， Data.Vect.Views 和 Data.Nat.Views .

  回复于 2024-04-29T03:10:07+08:00
• 7

  仅供参考：idris 1.3.0（可能是1.2.0）的实现是完全的，但是使用assert_total函数来实现这一点 .

  :printdef gcd
  gcd : (a : Nat) ->
        (b : Nat) -> {auto ok : NotBothZero a b} -> Nat
  gcd a 0 = a
  gcd 0 b = b
  gcd a (S b) = assert_total (gcd (S b)
                                  (modNatNZ a (S b) SIsNotZ))
  

  回复于 2024-04-29T03:10:07+08:00