Induction

Suppose P is a predicate on terms.

Induction on depth:

If, for each term s,

given P(r) for all r such that depth(r) < depth(s)

we can show P(s),

then P(s) holds for all s.

Induction on size:

If, for each term s,

given P(r) for all r such that size(r) < size(s)

we can show P(s),

then P(s) holds for all s.

Structural induction:

If, for each term s,

given P(r) for all immediate subterms r of s

we can show P(s),

then P(s) holds for all s.

pl
Unless otherwise stated, the content of this page is licensed under Creative Commons Attribution-ShareAlike 3.0 License