beta_conv : term -> term
STRUCTURE
Term
SYNOPSIS
Performs one step of beta-reduction.
DESCRIPTION
Beta-reduction is one of the primitive operations in the lambda calculus. A step of beta-reduction may be performed by beta_conv M, where M is the application of a lambda abstraction to an argument, i.e., has the form ((\v.N) P). The beta-reduction occurs by systematically replacing every free occurrence of v in N by P.

Care is taken so that no free variable of P becomes captured in this process.

FAILURE
If M is not the application of an abstraction to an argument.
EXAMPLE
- beta_conv (mk_comb (Term `\(x:'a) (y:'b). x`, Term `(P:bool -> 'a) Q`));
> val it = `\y. P Q` : term

- beta_conv (mk_comb (Term `\(x:'a) (y:'b) (y':'b). x`, Term `y:'a`));
> val it = `\y'. y` : term

COMMENTS
More complex strategies for coding up full beta-reduction can be coded up in ML. The conversions of Larry Paulson support this activity as inference steps.
USES
For programming derived rules of inference.
SEEALSO
BETA_CONV, RIGHT_BETA, LIST_BETA_CONV, RIGHT_LIST_BETA, DEPTH_CONV, TOP_DEPTH_CONV, REDEPTH_CONV
HOL  Kananaskis-13