CODEWITHSUNDEEP
isabelleinductionnon-termination
Sebastian Graf
Sebastian Graf

Reputation: 3740

Non-terminating inductive predicates

In the excellent Programming and Proving in Isabelle/HOL it says

[...] in contrast to recursive functions, there is no termination requirement for inductive definitions. (pdf p. 40)

  1. Does this mean there are inductive definitions where it's possible to have an infinitely deep derivation tree?
  2. What is an example of such a non-terminating derivation (preferably one with infinite height)? How do you 'construct' these?
  3. How are rule induction principles on these still sound?

Upvotes: 0

Views: 213

Answers (2)

Manuel Eberl
Manuel Eberl

Reputation: 8278

Lars already answered the question, but I would like to expand on the coinductive predicates he mentioned. These indeed allow you to have ‘infinitely deep derivation trees’, corresponding to how codatatypes are essentially ‘possibly infinite datatypes’.

A good example is the stream type from ~~/src/HOL/Library/Stream:

codatatype 'a stream = SCons 'a "'a stream" (infixr "##" 65)

This is an infinite list (note that unlike e.g. Haskell lists, this stream type has to be infinitely long, like if you wrote datatype Stream a = SCons a (Stream a) in Haskell, although Haskell-style ‘potentially infinite’ lists are also possible straightforward, cf. the lazy lists in the AFP)

You can then e.g. define the set of all streams whose values are from a given set. You could define that as streams A = {s. sset s ⊆ A}, but in Isabelle, it is defined coinductively like this:

coinductive_set streams :: "'a set ⇒ 'a stream set" for A :: "'a set"
  where "⟦a ∈ A; s ∈ streams A⟧ ⟹ a ## s ∈ streams A"

Another, perhaps easier example, would be a coinductive ‘for all elements’ predicate on streams:

coinductive sall :: "('a ⇒ bool) ⇒ 'a stream ⇒ bool" for P :: "'a ⇒ bool" where
  "P x ⟹ sall P xs ⟹ sall P (x ## xs)"

As for the question of how to construct such an infinite derivation tree, i.e. showing that a coinductive predicate holds on some value, you have to do that with coinduction. E.g. we can show that if P x holds, then sall P (sconst x) holds, where sconst x is just the value x repeated infinitely:

lemma sconst_reduce: "sconst x = x ## sconst x"
  by (subst siterate.code) simp_all

lemma sall_sconst: "P x ⟹ sall P (sconst x)"
proof (coinduction rule: sall.coinduct)
  assume "P x"
  thus "∃y ys. sconst x = y ## ys ∧ P y ∧ (ys = sconst x ∧ P x ∨ sall P ys)"
    by (subst sconst_reduce) auto
qed

Upvotes: 2

larsrh
larsrh

Reputation: 2659

  1. No. You need coinductive predicates for that.
  2. Not existing.
  3. If you look at the induction principle, you'll find that they have an additional premise. For example, "even n". That means, before you can even apply the induction principle, you'll need to know that you have a finite derivation at hand.

Upvotes: 2

Related Questions