Блог

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

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

Я удовлетворен тем, что это гарантирует завершение, но Agda не так легко убедить.

  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, что эта функция (и другие подобные функции, использующие ту же идею) завершится? (В идеале без слишком большого изменения типов данных.)

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