12,080
edits
Changes
MyWikiBiz, Author Your Legacy — Wednesday November 20, 2024
Jump to navigationJump to searchDirectory:Jon Awbrey/Papers/Cactus Language (view source)
Revision as of 14:32, 1 June 2009
, 14:32, 1 June 2009→Note 7: markup + rewrite
<br>
<br>
The shift operator <math>\operatorname{E}</math> can be understood as enacting a ''substitution operation'' on the proposition that is given as its argument.
The shift operator E can be understood as enacting a substitution operation
on the proposition that is given as its argument. In our immediate example,
E : (U -> B) -> (EU -> B),
For example, the action of <math>\operatorname{E}</math> on the conjunction <math>f(x, y) = xy\!</math> is defined as follows:
E : f(x, y) -> Ef(x, y, dx, dy),
{| align="center" cellpadding="6" width="90%"
|
<math>\begin{array}{lcl}
\operatorname{E} : (U \to \mathbb{B})
& \to &
(\operatorname{E}U \to \mathbb{B}),
\\[6pt]
\operatorname{E} : f(x, y)
& \mapsto &
\operatorname{E}f(x, y, \operatorname{d}x, \operatorname{d}y),
\\[6pt]
\operatorname{E}f(x, y, \operatorname{d}x, \operatorname{d}y)
& = &
f(x + \operatorname{d}x, y + \operatorname{d}y).
\end{array}</math>
|}
Therefore, if we evaluate <math>\operatorname{E}f</math> at particular values of <math>\operatorname{d}x</math> and <math>\operatorname{d}y,</math> for example, <math>\operatorname{d}x = i</math> and <math>\operatorname{d}y = j,</math> where <math>i, j \in \mathbb{B},</math> we obtain:
{| align="center" cellpadding="6" width="90%"
| <math>\operatorname{E}_{ij} : (U \to \mathbb{B}) \to (U \to \mathbb{B}),</math>
|-
| <math>\operatorname{E}_{ij} : f \mapsto \operatorname{E}_{ij}f,</math>
|-
| <math>\operatorname{E}_{ij}f = \operatorname{E}f|_{\operatorname{d}x = i, \operatorname{d}y = j} = f(x + i, y + j).</math>
|}
<pre>
The notation is a little bit awkward, but the data of the Table should
The notation is a little bit awkward, but the data of the Table should
make the sense clear. The important thing to observe is that E_ij has
make the sense clear. The important thing to observe is that E_ij has
