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