1\DOC PBETA_CONV
2
3\TYPE {PBETA_CONV : conv}
4
5\SYNOPSIS
6Performs a general beta-conversion.
7
8\KEYWORDS
9conversion.
10
11\DESCRIBE
12The conversion {PBETA_CONV} maps a paired beta-redex {"(\p.t)q"} to the theorem
13{
14   |- (\p.t)q = t[q/p]
15}
16where {u[q/p]} denotes the result of substituting {q} for all free
17occurrences of {p} in {t}, after renaming sufficient bound variables to avoid
18variable capture.
19Unlike {PAIRED_BETA_CONV}, {PBETA_CONV} does not require that the structure
20of the argument match the structure of the pair bound by the abstraction.
21However, if the structure of the argument does match the structure of the
22pair bound by the abstraction, then {PAIRED_BETA_CONV} will do the job
23much faster.
24
25\FAILURE
26{PBETA_CONV tm} fails if {tm} is not a paired beta-redex.
27
28\EXAMPLE
29{PBETA_CONV} will reduce applications with arbitrary structure.
30{
31   - PBETA_CONV
32        (Term `((\((a:'a,b:'a),(c:'a,d:'a)). f a b c d) ((w,x),(y,z))):'a`);
33   > val it = |- (\((a,b),c,d). f a b c d) ((w,x),y,z) = f w x y z : thm
34}
35
36{PBETA_CONV} does not require the structure of the argument and the bound
37pair to match.
38{
39   - PBETA_CONV
40       (Term `((\((a:'a,b:'a),(c:'a,d:'a)). f a b c d) ((w,x),yz)):'a`);
41   > val it = |- (\((a,b),c,d). f a b c d) ((w,x),yz) =
42                 f w x (FST yz) (SND yz) : thm
43}
44
45{PBETA_CONV} regards component pairs of the bound pair as variables in their
46own right and preserves structure accordingly:
47{
48   - PBETA_CONV
49       (Term `((\((a:'a,b:'a),(c:'a,d:'a)). f (a,b) (c,d)) (wx,(y,z))):'a`);
50   > val it = |- (\((a,b),c,d). f (a,b) (c,d)) (wx,y,z) = f wx (y,z) : thm
51}
52
53
54\SEEALSO
55Thm.BETA_CONV, PairedLambda.PAIRED_BETA_CONV, PairRules.PBETA_RULE, PairRules.PBETA_TAC, PairRules.LIST_PBETA_CONV, PairRules.RIGHT_PBETA, PairRules.RIGHT_LIST_PBETA, PairRules.LEFT_PBETA, PairRules.LEFT_LIST_PBETA.
56\ENDDOC
57