CODEWITHSUNDEEP
isabelletermination
best wish
best wish

Reputation: 55

isabelle termination with distance of real numbers

maybe someone can help me with a termination proof in Isabelle. I am trying to construct from the list A a new sub-list B. For constructing B, I read again and again of the whole A. Take out elements and use the result for the search for the next element. I designed a simple example to illustrate that:

given is a list of random real numbers. And we say that a number P is on the list, if an item from the list is greater than P.

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

I create a function that always take the next larger element.

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

And now I'm trying to create a new sorted part-list by take out the next larger element than P but less than Q with nextPoint and continuing with this.

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([]))"

I have already demonstrated nextPoint always returns a growing number:

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

the termination proof with relation "measure (size o fst o snd)“ not working for real numbers…and now I don’t know how to continue.

Upvotes: 0

Views: 139

Answers (2)

Manuel Eberl
Manuel Eberl

Reputation: 8278

To show termination in Isabelle, you have to show that the recursive calls follow a wellfounded relation. The easiest way to do that is to give a termination measure returning natural number that becomes smaller with every call. That does not work with real numbers because they are not wellfounded – you could have something like 1 → 1/2 → 1/4 → 1/8 → …

The termination measure to use in your case would be the number of list elements that fulfil the condition, i.e. length (filter (λx. P ≤ x ∧ x ≤ Q)) l. However, note that your definition fails to work if Q is larger than all numbers in the list.

Your definition is somewhat laborious and complicated. I recommend the following definition:

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

or, equivalently, 

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

Note, however, that this definition does not throw away multiple occurrences of the same number, i.e. listBetween L 0 10 [2,1,2] = [1,2,2]. If you want to throw them away, you can use remdups.

Also note that something like pointOnList L P ≡ ∃ i. i < length L ∧ P < L!i is pretty much never what you want – there is no need to work with explicit list indices here. Just do ∃x∈set L. P < x.

Upvotes: 2

Ren&#233; Thiemann
Ren&#233; Thiemann

Reputation: 1271

The termination argument relation "measure (size o fst o snd)" does not work for several reasons:

  • With your lemma foo you have just proven that the value increases. But for termination you need a decreasing measure. So you might want to use the difference

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

  • Even then there is the problem that measure expects a mapping into the natural numbers and Q - P is a real number, so this does not work. You used size before, but your lemma foo states nothing about the connection between size and <. Moreover, < is not a well-founded order over the real numbers.

  • Eventually, I would try to avoid the reasoning on reals in this simple example at all and take as measure something like

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

    and adapt the statement of foo accordingly.

Upvotes: 1

Related Questions