beta_conv
Term.beta_conv : term -> term
Performs one step of beta-reduction.
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'. 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.
For programming derived rules of inference.
See also
Thm.BETA_CONV,
Drule.RIGHT_BETA,
Drule.LIST_BETA_CONV,
Drule.RIGHT_LIST_BETA,
Conv.DEPTH_CONV,
Conv.TOP_DEPTH_CONV,
Conv.REDEPTH_CONV