Доказательство завершения с функциями, использующими понимание множеств

Рассмотрим следующее глупое определение Изабель деревьев и поддеревьев:

datatype tree = Leaf int
              | Node tree tree

fun children :: "tree ⇒ tree set" where
"children (Leaf _) = {}" |
"children (Node a b) = {a, b}"

lemma children_decreasing_size:
  assumes "c ∈ children t"
  shows   "size c < size t"
using assms
by (induction t, auto)

function subtrees :: "tree ⇒ tree set" where
"subtrees t = { s | c s. c ∈ children t ∧ s ∈ subtrees c }"
by auto
termination
apply (relation "measure size", simp)

Доказательство завершения subtrees застревает на этом этапе, хотя рекурсивные вызовы всегда выполняются только для дочерних элементов, которые строго меньше по хорошо обоснованному отношению size (как показывает тривиальная лемма).

Состояние доказательства следующее:

goal (1 subgoal):
 1. ⋀t x xa xb. (xa, t) ∈ measure size

Конечно, это невозможно доказать, поскольку информация о том, что xa является потомком t, потеряна. Я сделал что-то не так? Могу ли я что-нибудь сделать, чтобы сохранить доказательство? Замечу, что я могу сформулировать то же определение, используя списки вместо наборов:

fun children_list :: "tree ⇒ tree list" where
"children_list (Leaf _) = []" |
"children_list (Node a b) = [a, b]"

function subtrees_list :: "tree ⇒ tree list" where
"subtrees_list t = concat (map subtrees_list (children_list t))"
by auto
termination
apply (relation "measure size", simp)

и получите более информативную и доказуемую цель увольнения:

goal (1 subgoal):
 1. ⋀t x.
       x ∈ set (children_list t) ⟹
       (x, t) ∈ measure size

Это какое-то ограничение в Изабель, которое я должен просто обойти, не используя для этого наборы?


termination isabelle
person Isabelle Newbie    schedule 27.10.2015    source источник
comment
Знаете ли вы, что, согласно вашему определению, subtrees всегда возвращает пустой набор?   -  person Manuel Eberl    schedule 28.10.2015
comment
Хех, хороший улов. Это было упрощено (слишком сильно) из чего-то более сложного, что я пытаюсь сделать.   -  person Isabelle Newbie    schedule 28.10.2015

Ответы (1)


arrow_upward
3
arrow_downward

Ограничение c : children t в понимании набора для subtrees не проявляется в обязательстве доказательства прекращения, потому что пакет функций ничего априори не знает о &. Для этого можно использовать правила конгруэнтности. В этом случае вы можете локально объявить conj_cong как [fundef_cong], чтобы имитировать порядок оценки слева направо (хотя в HOL нет такой вещи, как оценка). Например,

context notes conj_cong[fundef_cong] begin
fun subtrees :: ...
termination ...
end

Блок контекста гарантирует, что объявление conj_cong[fundef_cong] действует только для этого определения функции.

Версия со списками работает, потому что в ней используется функция map, для которой по умолчанию действует правило сравнения. То же самое должно было сработать для наборов, если бы вы использовали операцию монадического связывания для наборов (а не понимание набора).

person Andreas Lochbihler    schedule 28.10.2015
comment
Другое определение, которое работает: subtrees t = (⋃c∈children t. subtrees c). Однако я бы сказал, что с примитивно-рекурсивным определением, вероятно, легче работать. - person Manuel Eberl; 28.10.2015
comment
@Manuel Eberl: Union - это монадическая привязка для множеств, поэтому ваше предложение - это именно то, о чем я имел в виду в своем последнем предложении. - person Andreas Lochbihler; 28.10.2015
comment
О верно. конечно. Я этого не заметил. В любом случае, это может быть очевидным не для всех читателей. - person Manuel Eberl; 28.10.2015
comment
Спасибо вам обоим. Выспавшись на нем, я тоже пришел к идее использовать (⋃c∈children t. subtrees c), хотя я бы и не догадался, что это то, что означает монадическое связывание в данном контексте. Так что спасибо за разъяснения. - person Isabelle Newbie; 28.10.2015
comment
Фактически, если быть точным, Union - это монадическое соединение для множеств. Но привязку, конечно, можно определить с помощью join и map, где map - операция установки изображения. - person Manuel Eberl; 30.10.2015