Убедить Идриса в совокупности рекурсивных вызовов - PullRequest
Новая
       21

Убедить Идриса в совокупности рекурсивных вызовов

0 голосов
/ 16 февраля 2019

Я написал следующий тип для кодирования всех возможных рациональных чисел в нем: 

data Number : Type where
    PosN : Nat -> Number
    Zero : Number
    NegN : Nat -> Number
    Ratio : Number -> Number -> Number

Обратите внимание, что PosN Z на самом деле кодирует число 1, а NegN Z кодирует -1.Я предпочитаю такое симметричное определение тому, что дано модулем Data.ZZ.Теперь у меня есть проблема с убеждением Идриса, что добавление таких чисел является полным: 

mul : Number -> Number -> Number
mul Zero _ = Zero
mul _ Zero = Zero
mul (PosN k) (PosN j) = PosN (S k * S j - 1)
mul (PosN k) (NegN j) = NegN (S k * S j - 1)
mul (NegN k) (PosN j) = NegN (S k * S j - 1)
mul (NegN k) (NegN j) = PosN (S k * S j - 1)
mul (Ratio a b) (Ratio c d) = Ratio (a `mul` b) (c `mul` d)
mul (Ratio a b) c = Ratio (a `mul` c) b
mul a (Ratio b c) = Ratio (a `mul` b) c

plus : Number -> Number -> Number
plus Zero y = y
plus x Zero = x
plus (PosN k) (PosN j) = PosN (k + j)
plus (NegN k) (NegN j) = NegN (k + j)
plus (PosN k) (NegN j) = subtractNat k j
plus (NegN k) (PosN j) = subtractNat j k
plus (Ratio a b) (Ratio c d) =
    let a' = assert_smaller (Ratio a b) a in
    let b' = assert_smaller (Ratio a b) b in
    let c' = assert_smaller (Ratio c d) c in
    let d' = assert_smaller (Ratio c d) d in
    Ratio ((mul a' d') `plus` (mul b' c')) (mul b' d')
plus (Ratio a b) c =
    let a' = assert_smaller (Ratio a b) a in
    let b' = assert_smaller (Ratio a b) b in
    Ratio (a' `plus` (mul b' c)) c
plus a (Ratio b c) =
    let b' = assert_smaller (Ratio b c) b in
    let c' = assert_smaller (Ratio b c) c in
    Ratio ((mul a c') `plus` b') (mul a c')

Интересно, когда я нажимаю Alt-Ctrl-R в редакторе Atom, все нормально (даже с директивой %default total),Однако, когда я загружаю это в REPL, он предупреждает меня, что plus, возможно, не является полным: 

   |
29 |     plus Zero y = y
   |     ~~~~~~~~~~~~~~~
Data.Number.NumType.plus is possibly not total due to recursive path 
Data.Number.NumType.plus --> Data.Number.NumType.plus

Из сообщения я понимаю, что он обеспокоен этими рекурсивными вызовами plus в коэффициентах обработки шаблонов,Я думал, что утверждение, что a меньше, чем Ratio a b и т. Д., Решит проблему, но это не так, поэтому, вероятно, Идрис видит это, но имеет проблемы с чем-то другим.Хотя я не могу понять, что это может быть.

1 Ответ

0 голосов
/ 16 февраля 2019

assert_smaller (Ratio a b) a уже известен Идрису (a в конце концов является аргументом для «большего» типа Ratio a b).Что вам нужно доказать (или утверждать), так это то, что результат mul структурно меньше аргументов для plus.

Так что он должен работать с 

plus (Ratio a b) (Ratio c d) =
    let x = assert_smaller (Ratio a b) (mul a d) in
    let y = assert_smaller (Ratio a b) (mul b c) in
    Ratio (x `plus` y) (mul b d)
plus (Ratio a b) c =
    let y = assert_smaller (Ratio a b) (mul b c) in
    Ratio (a `plus` y) c
plus a (Ratio b c) =
    let x = assert_smaller (Ratio b c) (mul a c) in
    Ratio (x `plus` b) (mul a c)
...