text‹\noindent
index{measure functions}%
definition of @{term"fib"} is accompanied by a \textbf{measure function}
{term"%n. n"} which maps the argument of @{term"fib"} to a
number. The requirement is that in each equation the measure of the
on the left-hand side is strictly greater than the measure of the
of each recursive call. In the case of @{term"fib"} this is
true because the measure function is the identity and
{term"Suc(Suc x)"} is strictly greater than both @{term"x"} and
{term"Suc x"}.
more interesting is the insertion of a fixed element
any two elements of a list: ›
consts sep :: "'a × 'a list ==> 'a list" recdef sep "measure (λ(a,xs). length xs)" "sep(a, []) = []" "sep(a, [x]) = [x]" "sep(a, x#y#zs) = x # a # sep(a,y#zs)"
text‹\noindent
time the measure is the length of the list, which decreases with the
call; the first component of the argument tuple is irrelevant.
details of tupled $\lambda$-abstractions ‹λ(x1,…,xn)› are
in \S\ref{sec:products}, but for now your intuition is all you need.
matching\index{pattern matching!and \isacommand{recdef}}
not be exhaustive: ›
consts last :: "'a list ==> 'a" recdef last "measure (λxs. length xs)" "last [x] = x" "last (x#y#zs) = last (y#zs)"
text‹
patterns are disambiguated by taking the order of equations into
, just as in functional programming: ›
consts sep1 :: "'a × 'a list ==> 'a list" recdef sep1 "measure (λ(a,xs). length xs)" "sep1(a, x#y#zs) = x # a # sep1(a,y#zs)" "sep1(a, xs) = xs"
text‹\noindent
guarantee that the second equation can only be applied if the first
does not match, Isabelle internally replaces the second equation
the two possibilities that are left: @{prop"sep1(a,[]) = []"} and
{prop"sep1(a, [x]) = [x]"}. Thus the functions @{term sep} and
{const sep1} are identical.
begin{warn} \isacommand{recdef} only takes the first argument of a (curried)
recursive function into account. This means both the termination measure
and pattern matching can only use that first argument. In general, you will
therefore have to combine several arguments into a tuple. In case only one
argument is relevant for termination, you can also rearrange the order of
arguments as in the following definition:
end{warn} › consts sep2 :: "'a list ==> 'a ==> 'a list" recdef sep2 "measure length" "sep2 (x#y#zs) = (λa. x # a # sep2 (y#zs) a)" "sep2 xs = (λa. xs)"
text‹
of its pattern-matching syntax, \isacommand{recdef} is also useful
the definition of non-recursive functions, where the termination measure
to the empty set @{term"{}"}: ›
consts swap12 :: "'a list ==> 'a list" recdef swap12 "{}" "swap12 (x#y#zs) = y#x#zs" "swap12 zs = zs"
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
