Version française
Home     About     Download     Resources     Contact us    
Browse thread
Pervasives or Printf module ?
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Remi Vanicat <remi.vanicat@g...>
Subject: Re: [Caml-list] Re: Pervasives or Printf module ?
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.