Полное определение Gcd в Идрисе - PullRequest
Новая
       8

Полное определение Gcd в Идрисе

0 голосов
/ 03 июня 2018

Я работаю в небольшом проекте с целью дать определение Gcd, которое дает gcd из двух чисел вместе с доказательством правильности результата.Но я не могу дать полное определение Gcd.Определение Gcd в Idris 1.3.0 является полным, но использует assert_total для принудительного определения тотальности, которая противоречит цели моего проекта.У кого-то есть полное определение Gcd, которое не использует assert_total?

PS - Мои коды загружены в https://github.com/anotherArka/Idris-Number-Theory.git

Ответы [ 2 ]

0 голосов
/ 03 июня 2018

У меня есть версия, которая использует отношение 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.

0 голосов
/ 03 июня 2018

К вашему сведению: реализация в 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))
...