2006/1/22, Vincenzo Ciancia <vincenzo_yahoo_addressguard-gmane@yahoo.it>:
> Jon Harrop wrote:
>
> > To get the latter to act as the former
> > does, you must beta expand (I think that is the correct technical term)
>
> In computer science literature, alpha conversion is usually the renaming of
> a bound variable (fun x -> T = fun y -> T[y/x] provided that y does not
> occurr in T), beta _reduction_ is function application ((fun x -> T)(T') =
> T[T'/x]) , and _eta_ expansion is the term rewriting you're looking for.
>
> I don't know why, maybe it's just the order in which they were enumerated
> originarily, but where are gamma, delta, epsilon, zeta rewrite rules? :)

In the coq manual, one can see severall other rewriting rule, like
iota-reduction, delta-reduction and zeta-reduction.