Как убедить Агду, что функция заканчивается сокращением числа внутри пары? - PullRequest
Новая
       9

Как убедить Агду, что функция заканчивается сокращением числа внутри пары?

1 голос
/ 04 апреля 2019

Я кодирую и проверяю правильность части генерации кода компилятора в Agda. Мне трудно убедить Агду, что некоторые из моих функций прекращаются. Язык высокого уровня, который я использую, имеет циклы while, поэтому, очевидно, что для любой программы нет гарантии его завершения.

Из-за этого я использую переменную «fuel», которая является просто натуральным числом и уменьшается на единицу при выполнении каждого выражения, ограничивая количество шагов, для которых может выполняться программа.

Я удовлетворен тем, что это гарантирует прекращение, но Агда не так легко убедить. 

 data Stateᴴᴸ : Set where
   stateᴴᴸ : Store → (fuel : ℕ) → Stateᴴᴸ

 {-# TERMINATING #-}
 storeᴴᴸ' : IExp → Stateᴴᴸ → Stateᴴᴸ
 storeᴴᴸ' i (stateᴴᴸ σ 0)                           = stateᴴᴸ σ 0
 storeᴴᴸ' SKIP                  (stateᴴᴸ σ (suc f)) = stateᴴᴸ σ f
 storeᴴᴸ' (x ≔ a)               (stateᴴᴸ σ (suc f)) = stateᴴᴸ ((x ≔ aexe a σ) ∷ σ) f
 storeᴴᴸ' (P ⋯ Q)               state = storeᴴᴸ' Q (storeᴴᴸ' P state)
 storeᴴᴸ' (IF b THEN P ELSE Q) (stateᴴᴸ σ (suc f)) with bexe b σ
 ... | true  = storeᴴᴸ' P (stateᴴᴸ σ f)
 ... | false = storeᴴᴸ' Q (stateᴴᴸ σ f)
 storeᴴᴸ' (WHILE b DO c)       (stateᴴᴸ σ (suc f)) with bexe b σ
 ... | true  = storeᴴᴸ' (c ⋯ (WHILE b DO c)) (stateᴴᴸ σ f)
 ... | false = stateᴴᴸ σ f

В приведенном выше коде я должен использовать завершающую прагму, в противном случае Agda подаст следующую жалобу: 

Termination checking failed for the following functions:
  storeᴴᴸ'
Problematic calls:
  storeᴴᴸ' Q (storeᴴᴸ' P state)
  storeᴴᴸ' P state
  storeᴴᴸ' (c ⋯ (WHILE b DO c)) (stateᴴᴸ σ f)

Сначала я думал, что это потому, что мой тип данных Stateᴴᴸ не имеет рекурсивной структуры, которую имеет ℕ. Поэтому я изменил его следующим образом: 

  data Stateᴴᴸ : Set where
    stateᴴᴸ : Store  → Stateᴴᴸ
    sucstateᴴᴸ : Stateᴴᴸ → Stateᴴᴸ

И соответственно изменил функцию; но это не решило проблему.

Как я могу убедить Agda, что эта функция (и другие подобные функции, использующие ту же идею) завершатся? (В идеале, без слишком большого изменения типов данных.)

1 Ответ

2 голосов
/ 04 апреля 2019

Вы делаете структурную рекурсию по двум аргументам: структура вашего выражения и топливо.Иногда топливо снижается, а иногда выражение уменьшается, но это не тот случай, когда другой остается прежним.Это вообще не прекращение.Вы можете делать рекурсию только по лексическому произведению заказов.

...