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