Idris 中 Gcd 的总定义

Question

我在一个小项目中工作，目标是给出 Gcd 的定义，它给出了两个数字的 gcd 以及结果正确的证明。但我无法给出 Gcd 的完整定义。 Idris 1.3.0 中 Gcd 的定义是完全的，但使用 assert_total 来强制完全性，这违背了我项目的目的。有人有不使用assert_total的Gcd的总定义吗？

P.S。 - 我的代码已上传到 https://github.com/anotherArka/Idris-Number-Theory.git

Answer 1

仅供参考：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))

Answer 2

我有一个版本，它使用 Accessible 关系来表明你找到的两个数字的总和在每次递归调用时都会变小：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 在序言中定义，并允许您在此处明确声明它是越来越小的输入总和。递归调用小于输入，因为 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，至少对于 Idris（您可能会找到 Coq 的示例），但是 base 库中有更多示例Data.List.Views、Data.Vect.Views 和 Data.Nat.Views.

Idris 中 Gcd 的总定义

Total definition of Gcd in Idris

idris