12,080
edits
Changes
Directory:Jon Awbrey/Papers/Syntactic Transformations (view source)
Revision as of 15:57, 3 February 2009
, 15:57, 3 February 2009→Syntactic Transformation Rules: format rule box
<br>
<br>
<pre>
{| align="center" cellpadding="0" cellspacing="0" style="border-left:1px solid black; border-top:1px solid black; border-right:1px solid black; border-bottom:1px solid black" width="90%"
Rule 11
|
{| align="center" cellpadding="0" cellspacing="0" width="100%"
|- style="height:40px; text-align:center"
| width="80%" |
| width="20%" style="border-left:1px solid black" | <math>\operatorname{Rule~11}</math>
|}
|-
|
{| align="center" cellpadding="0" cellspacing="0" width="100%"
|- style="height:40px"
| width="2%" style="border-top:1px solid black" |
| width="18%" style="border-top:1px solid black" | <math>\text{If}\!</math>
| width="60%" style="border-top:1px solid black" | <math>Q ~\subseteq~ X</math>
| width="20%" style="border-top:1px solid black; border-left:1px solid black" |
|- style="height:40px"
|
| <math>\text{then}\!</math>
| <math>\text{the following are equivalent:}\!</math>
| style="border-left:1px solid black" |
|}
|-
|
{| align="center" cellpadding="0" cellspacing="0" width="100%"
|- style="height:40px"
| width="2%" style="border-top:1px solid black" |
| width="18%" style="border-top:1px solid black" | <math>\operatorname{R11a.}</math>
| width="60%" style="border-top:1px solid black" | <math>Q ~=~ \{ x \in X ~:~ s \}</math>
| width="20%" style="border-top:1px solid black; border-left:1px solid black; text-align:center" | <math>\operatorname{R11a~:~R5a}</math>
|- style="height:20px"
|
|
|
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
|- style="height:40px"
|
| <math>\operatorname{R11b.}</math>
| <math>\upharpoonleft Q \upharpoonright ~=~ \upharpoonleft \{ x \in X ~:~ s \} \upharpoonright</math>
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R11b~:~R5e}</math>
|- style="height:20px"
|
|
|
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
|- style="height:60px"
|
| <math>\operatorname{R11c.}</math>
|
<math>\begin{array}{lcl}
\upharpoonleft Q \upharpoonright
& \subseteq &
X \times \underline\mathbb{B}
\\
\upharpoonleft Q \upharpoonright
& = &
\{ (x, y) \in X \times \underline\mathbb{B} ~:~ y = \, \downharpoonleft s \downharpoonright (x) \}
\end{array}</math>
| style="border-left:1px solid black; text-align:center" |
<p><math>\operatorname{R11c~:~\_\_?\_\_}</math></p>
<p><math>\operatorname{R11c~:~\_\_?\_\_}</math></p>
|- style="height:20px"
|
|
|
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
|- style="height:60px"
|
| <math>\operatorname{R11d.}</math>
|
<math>\begin{array}{ccccl}
\upharpoonleft Q \upharpoonright & : & X & \to & \underline\mathbb{B}
\\
\upharpoonleft Q \upharpoonright & : & x & \mapsto & \downharpoonleft s \downharpoonright (x)
\end{array}</math>
| style="border-left:1px solid black; text-align:center" |
<p><math>\operatorname{R11d~:~\_\_?\_\_}</math></p>
<p><math>\operatorname{R11d~:~\_\_?\_\_}</math></p>
|- style="height:20px"
|
|
|
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
|- style="height:60px"
|
| <math>\operatorname{R11e.}</math>
| <math>\overset{X}{\underset{x}{\forall}}~ \upharpoonleft Q \upharpoonright (x) ~=~ \downharpoonleft s \downharpoonright (x)</math>
| style="border-left:1px solid black; text-align:center" |
<p><math>\operatorname{R11e~:~\_\_?\_\_}</math></p>
<p><math>\operatorname{R11e~:~\_\_?\_\_}</math></p>
|- style="height:20px"
|
|
|
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
|- style="height:40px"
|
| <math>\operatorname{R11f.}</math>
| <math>\upharpoonleft Q \upharpoonright ~=~ \downharpoonleft s \downharpoonright</math>
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R11f~:~\_\_?\_\_}</math>
|}
|}
<br>
<pre>
An application of Rule 11 involves the recognition of an antecedent condition as a case under the Rule, that is, as a condition that matches one of the sentences in the Rule's chain of equivalents, and it requires the relegation of the other expressions to the production of a result. Thus, there is the choice of an initial expression that has to be checked on input for whether it fits the antecedent condition, and there is the choice of three types of output that are generated as a consequence, only one of which is generally needed at any given time. More often than not, though, a rule is applied in only a few of its possible ways. The usual antecedent and the usual consequents for Rule 11 can be distinguished in form and specialized in practice as follows:
An application of Rule 11 involves the recognition of an antecedent condition as a case under the Rule, that is, as a condition that matches one of the sentences in the Rule's chain of equivalents, and it requires the relegation of the other expressions to the production of a result. Thus, there is the choice of an initial expression that has to be checked on input for whether it fits the antecedent condition, and there is the choice of three types of output that are generated as a consequence, only one of which is generally needed at any given time. More often than not, though, a rule is applied in only a few of its possible ways. The usual antecedent and the usual consequents for Rule 11 can be distinguished in form and specialized in practice as follows: