Изабель окончание с расстоянием действительных чисел

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

дан список случайных действительных чисел. И мы говорим, что число P находится в списке, если элемент из списка больше, чем P.

definition pointOnList :: "real list ⇒ real ⇒ bool" where
  "pointOnList L P ≡ ∃ i. i < length L ∧ P < L!i"

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

fun nextPoint :: "real list ⇒ real ⇒ real" where
  "nextPoint (X#Ls) P = (if (X > P)
    then (X)
    else (nextPoint Ls P))"

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

function listBetween :: "real list ⇒ real ⇒ real ⇒ real list" where
  "pointOnList L P ⟹ pointOnList L Q ⟹ listBetween L P Q = (if(P ≤ Q)
  then(P # (listBetween L (nextPoint L P) Q))
  else([]))"

Я уже продемонстрировал, что nextPoint всегда возвращает растущее число:

lemma foo: "pointOnList P A ⟹ A < (nextPoint P A)"

доказательство прекращения с relation "measure (size o fst o snd)“ не работает для действительных чисел ... и теперь я не знаю, как продолжить.


termination isabelle
person best wish    schedule 21.09.2015    source источник

Ответы (2)


arrow_upward
2
arrow_downward

Чтобы показать завершение в Изабель, вы должны показать, что рекурсивные вызовы следуют хорошо обоснованному отношению. Самый простой способ сделать это - дать меру завершения, возвращающую натуральное число, которое становится меньше с каждым вызовом. Это не работает с действительными числами, потому что они недостаточно обоснованы - у вас может быть что-то вроде 1 → 1/2 → 1/4 → 1/8 →…

В качестве меры завершения в вашем случае будет использоваться количество элементов списка, удовлетворяющих условию, то есть length (filter (λx. P ≤ x ∧ x ≤ Q)) l. Однако обратите внимание, что ваше определение не работает, если Q больше всех чисел в списке.

Ваше определение несколько утомительно и сложно. Я рекомендую следующее определение:

listBetween L P Q = sort (filter (λx. P ≤ x ∧ x ≤ Q) L)

или, что то же самое,

listBetween L P Q = sort [x ← L. x ∈ {P..Q}]

Обратите внимание, однако, что это определение не отбрасывает несколько вхождений одного и того же числа, то есть listBetween L 0 10 [2,1,2] = [1,2,2]. Если вы хотите их выбросить, вы можете использовать remdups.

Также обратите внимание, что что-то вроде pointOnList L P ≡ ∃ i. i < length L ∧ P < L!i практически никогда не является тем, что вам нужно - здесь нет необходимости работать с явными индексами списка. Просто сделай ∃x∈set L. P < x.

person Manuel Eberl    schedule 21.09.2015

arrow_upward
1
arrow_downward

Аргумент завершения relation "measure (size o fst o snd)" не работает по нескольким причинам:

  • С помощью вашей леммы foo вы только что доказали, что значение увеличивается. Но для прекращения нужна убывающая мера. Так что вы можете захотеть использовать разницу

    relation "measure (λ (L,P,Q). Q - P)"

  • Даже в этом случае существует проблема, что measure ожидает отображения в натуральные числа, а Q - P является действительным числом, поэтому это не работает. Вы использовали size раньше, но ваша лемма foo ничего не говорит о связи между size и <. Более того, < не является обоснованным порядком над реальными числами.

  • В конце концов, я бы попытался вообще избежать рассуждений о действительных числах в этом простом примере и принять в качестве меры что-то вроде

    measure (λ (L,P,Q). length [ A . A <- L, P < A])"

    и соответствующим образом измените утверждение foo.

person René Thiemann    schedule 21.09.2015
comment
Это обозначение для понимания списка. Таким образом, это означает список, состоящий из элементов L в том же порядке, которые больше, чем P. - person Mathieu; 22.09.2015
comment
не удивляйтесь, я спросил, что означает [A ← L. P <A], и вскоре после этого удалил его. Спасибо за ваш быстрый ответ. - person best wish; 22.09.2015