beta_conv : term -> term

- STRUCTURE
- 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

HOL Kananaskis-14