伊德里斯Gcd的总体定义

Question

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

PS - 我的代码上传到 https://github.com/anotherArka/Idris-Number-Theory.git

Answer 1

我有一个使用该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在前奏中定义并允许您在此明确声明它是变小的输入的总和.递归调用小于输入,因为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.