Changes

There are two further reasons why it useful to spend time on a careful treatment of types, and they both have to do with our being able to take full computational advantage of certain dimensions of flexibility in the types that apply to terms.  First, the domains of differential geometry and logic programming are connected by analogies between real and boolean types of the same pattern.  Second, the types involved in these patterns have important isomorphisms connecting them that apply on both the real and the boolean sides of the picture.

There are two further reasons why it useful to spend time on a careful treatment of types, and they both have to do with our being able to take full computational advantage of certain dimensions of flexibility in the types that apply to terms.  First, the domains of differential geometry and logic programming are connected by analogies between real and boolean types of the same pattern.  Second, the types involved in these patterns have important isomorphisms connecting them that apply on both the real and the boolean sides of the picture.

Amazingly enough, these isomorphisms are themselves schematized by the axioms and theorems of propositional logic.  This fact is known as the ''propositions as types'' analogy or the Curry–Howard isomorphism [How].  In another formulation it says that terms are to types as proofs are to propositions.  See [LaS, 42–46] and [SeH] for a good discussion and further references.  To anticipate the bearing of these issues on our immediate topic, Table–3 sketches a partial overview of the Real to Boolean analogy that may serve to illustrate the paradigm in question.

Amazingly enough, these isomorphisms are themselves schematized by the axioms and theorems of propositional logic.  This fact is known as the ''propositions as types'' analogy or the Curry–Howard isomorphism [How].  In another formulation it says that terms are to types as proofs are to propositions.  See [LaS, 42–46] and [SeH] for a good discussion and further references.  To anticipate the bearing of these issues on our immediate topic, Table 3 sketches a partial overview of the Real to Boolean analogy that may serve to illustrate the paradigm in question.

{| align="center" border="1" cellpadding="8" cellspacing="0" style="font-weight:bold; text-align:center; width:96%"

{| align="center" border="1" cellpadding="8" cellspacing="0" style="font-weight:bold; text-align:center; width:96%"

| <math>\ldots\!</math>

| <math>\ldots\!</math>

| <math>\ldots\!</math>

| <math>\ldots\!</math>

|}

|}<br>

<br>

The Table exhibits a sample of likely parallels between the real and boolean domains.  The central column gives a selection of terminology that I borrow from typical usage in differential geometry and extend in its meaning to the logical side of the Table.  These are the varieties of spaces that come up when we turn to analyzing the dynamics of processes that followe their courses through the states of an arbitrary space ''X''.  Moreover, when it becomes necessary to approach situations of overwhelming dynamic complexity in a succession of qualitative reaches, then the methods of logic that are afforded by the boolean domains, with their declarative means of synthesis and deductive modes of analysis, supply a natural battery of tools for the task.

The Table exhibits a sample of likely parallels between the real and boolean domains.  The central column gives a selection of terminology that is borrowed from differential geometry and extended in its meaning to the logical side of the Table.  These are the varieties of spaces that come up when we turn to analyzing the dynamics of processes that followe their courses through the states of an arbitrary space <math>X.\!</math> Moreover, when it becomes necessary to approach situations of overwhelming dynamic complexity in a succession of qualitative reaches, then the methods of logic that are afforded by the boolean domains, with their declarative means of synthesis and deductive modes of analysis, supply a natural battery of tools for the task.

It is usually expedient to take these spaces two at a time, in dual pairs of the form ''X'' and (''X''&nbsp;&rarr;&nbsp;'''K'''). In general, one creates pairs of type schemas by replacing any space ''X'' with its dual (''X''&nbsp;&rarr;&nbsp;'''K'''), for example, pairing the type ''X''&nbsp;&rarr;&nbsp;''Y'' with the type (''X''&nbsp;&rarr;&nbsp;'''K''')&nbsp;&rarr;&nbsp;(''Y''&nbsp;&rarr;&nbsp;'''K'''), and ''X''&nbsp;&times;&nbsp;''Y'' with (''X''&nbsp;&rarr;&nbsp;'''K''')&nbsp;&times;&nbsp;(''Y''&nbsp;&rarr;&nbsp;'''K''').  Here, I am using

It is usually expedient to take these spaces two at a time, in dual pairs of the form <math>X\!</math> and <math>(X \to \mathbb{K}).</math>  In general, one creates pairs of type schemas by replacing any space <math>X\!</math> with its dual <math>(X \to \mathbb{K}),</math> for example, pairing the type <math>X \to Y</math> with the type <math>(X \to \mathbb{K}) \to (Y \to \mathbb{K}),</math> and <math>X \times Y</math> with <math>(X \to \mathbb{K}) \times (Y \to \mathbb{K}).</math> The word ''dual'' is used here in its broader sense to mean all of the functionals, not just the linear ones.  Given any function <math>f : X \to \mathbb{K},</math> the ''converse'' or inverse relation corresponding to <math>f\!</math> is denoted <math>f^{-1},\!</math> and the subsets of <math>X\!</math> that are defined by <math>f^{-1}(k),\!</math> taken over <math>k \in \mathbb{K},</math> are called the ''fibers'' or the ''level sets'' of the function <math>f.\!</math>

the word ''dual'' in its larger sense to mean all of the functionals, not just the linear ones.  Given any function ''f''&nbsp;:&nbsp;''X''&nbsp;&rarr;&nbsp;'''K''', the ''converse'' or inverse relation corresponding to ''f'' is denoted as ''f''^&ndash;1, and the subsets of ''X'' that are defined by ''f''^&ndash;1(''k''), taken over ''k'' in '''K''', are called the ''fibers'' or the ''level sets'' of the function ''f''.

===Theory of Control and Control of Theory===

===Theory of Control and Control of Theory===