If ≺ is a
well-ordering on the set S, then the height of an element
t∈S, written ht(t), is the
order type of {s∈S|s≺t}.
The height of S, ht(S), is the order type of (S,≺).
In the case of a relation which is only
well-founded, say ⊰ on S, the definition of
height is ht(t)=sup{ht(s)+1|s⊰t}.
Here the function sup is the supremum which calculates the least number greater than or equal to all of
the numbers of
the argument set, e.g. sup{1,2,3,4}=4.
The height is then the order type of the longest path.
The height of (S,⊰) is defined as ht(s)=sup{ht(s)+1|s∈S}.
Doets, Kees. From Logic to Logic Programming. MIT Press, 1994.
Copyright © 2014 Barry Watson. All rights reserved.