Well-founded recursion.
This is to let us implement some functions that don't have trivial
recursion patterns over datatypes, but instead are using some
other metric of size.
Accessibility: some element x
is accessible if all y
such that
rel y x
are themselves accessible.
the type of elements
a relation on a
the acessible element
Accessibility
the accessible element
a demonstration that all smaller elements are also accessible
Interface of types with sized values.
The size is used for proofs of termination via accessibility.
A relation rel
on a
is well-founded if all elements of a
are
acessible.
An induction principle for accessibility.
This allows us to recurse over the subset of some type that is
accessible according to some relation, producing a dependent type
as a result.
the well-founded relation
how to take steps on reducing arguments
the starting point
A recursor over accessibility.
This allows us to recurse over the subset of some type that is
accessible according to some relation.
the well-founded relation
how to take steps on reducing arguments
the starting point
Proof of well-foundedness of Smaller
.
Constructs accessibility for any given element of a
, provided Sized a
.
Strong induction principle for sized types.
Strong recursion principle for sized types.
Use well-foundedness of a relation to write proofs
a well-founded relation
the motive for the induction
the induction step: take an element and its accessibility,
and give back a demonstration of P for that element,
potentially using accessibility
Use well-foundedness of a relation to write terminating operations.
a well-founded relation