12,080
edits
Changes
Directory:Jon Awbrey/Papers/Propositions As Types (view source)
Revision as of 14:45, 25 March 2009
, 14:45, 25 March 2009→Step 2: markup
\end{array}</math>
\end{array}</math>
|}
|}
In a contextual, implicit, or paraphrastic definition of this sort, the ''definiendum'' is the symbol to be defined, in this case, <math>^{\backprime\backprime} \operatorname{T} ^{\prime\prime},</math> and the ''definiens'' is the entire rest of the context, in this case, the frame <math>^{\backprime\backprime} y(xz) = x(y(z\underline{~~}))\, ^{\prime\prime},</math> that ostensibly defines, or as one says, is supposed to define the symbol <math>^{\backprime\backprime} \operatorname{T} ^{\prime\prime}</math> that we find in its slot. More loosely speaking, the side of the equation with the more known symbols may be called its ''defining'' side.
<pre>
<pre>
In order to find a minimal generic typing, start with the defining side
In order to find a minimal generic typing, start with the defining side
of the equation, freely assigning types in such a way that the successive
of the equation, freely assigning types in such a way that the successive