Main Page: Difference between revisions

From formulasearchengine
Jump to navigation Jump to search
No edit summary
No edit summary
Line 1: Line 1:
{{Refimprove|date=December 2009}}
In [[mathematics]], the '''tautological one-form''' is a special [[1-form]] defined on the [[cotangent bundle]] ''T''*''Q'' of a [[manifold]] ''Q''. The [[exterior derivative]] of this form defines a [[symplectic form]] giving ''T''*''Q'' the structure of a [[symplectic manifold]]. The tautological one-form plays an important role in relating the formalism of [[Hamiltonian mechanics]] and [[Lagrangian mechanics]]. The tautological one-form is sometimes also called the '''Liouville one-form''', the '''Poincaré one-form''', the '''[[canonical (disambiguation)|canonical]] one-form''', or the '''symplectic potential'''. A similar object is the [[canonical vector field]] on the [[tangent bundle]]. In [[algebraic geometry]] and [[complex geometry]] the term "canonical" is discouraged, due to confusion with the [[canonical class]], and the term "tautological" is preferred, as in [[tautological bundle]].
In [[mathematical logic]] and [[theoretical computer science]], a [[rewrite system]] has the '''strong normalization property''' (in short: the '''normalization property''') if every term is ''strongly normalizing''; that is, if every sequence of rewrites eventually terminates to a term in [[Normal form (term rewriting)|normal form]]. A rewrite system may also have the '''weak normalization property''', meaning that for every term, there exists at least one particular sequence of rewrites that eventually yields a normal form.


== Lambda calculus ==
In [[canonical coordinates]], the tautological one-form is given by
=== Untyped lambda calculus ===
The ''pure'' untyped [[lambda calculus]] does not satisfy the strong normalization property, and not even the weak normalization property. Consider the term <math>\lambda x . x x x</math>. It has the following rewrite rule: For any term <math>t</math>,


: <math>(\mathbf{\lambda} x . x x x) t \rightarrow t t t</math>
:<math>\theta = \sum_i p_i dq^i</math>


But consider what happens when we apply <math>\lambda x . x x x</math> to itself:
Equivalently, any coordinates on phase space which preserve this structure for the canonical one-form, up to a total differential ([[exact form]]), may be called canonical coordinates; transformations between different canonical coordinate systems are known as [[canonical transformation]]s.
{|
| <math>(\mathbf{\lambda} x . x x x) (\lambda x . x x x)</math>
| <math> \rightarrow (\mathbf{\lambda} x . x x x) (\lambda x . x x x) (\lambda x . x x x)</math>
|-
|
| <math>  \rightarrow (\mathbf{\lambda} x . x x x) (\lambda x . x x x) (\lambda x . x x x) (\lambda x . x x x)</math>
|-
|
| <math>  \rightarrow (\mathbf{\lambda} x . x x x) (\lambda x . x x x) (\lambda x . x x x) (\lambda x . x x x) (\lambda x . x x x)</math>
|-
|
| <math>\ldots\,</math>
|}


Therefore the term <math>(\lambda x . x x x) (\lambda x . x x x)</math> is not strongly normalizing.
The '''canonical symplectic form''', also known as the '''Poincaré two-form''', is given by


=== Typed lambda calculus ===
:<math>\omega = -d\theta = \sum_i dq^i \wedge dp_i</math>


Various systems of [[typed lambda calculus]] including the
The extension of this concept to general [[fibre bundle]]s is known as the [[solder form]].
[[typed lambda calculus|simply typed lambda calculus]], [[Jean-Yves Girard]]'s [[System F]], and [[Thierry Coquand]]'s [[calculus of constructions]] are strongly normalizing.


A lambda calculus system with the '''normalization property''' can be viewed as a programming language with the property that every program [[termination analysis|terminates]]. Although this is a very useful property, it has a drawback: a programming language with the normalization property cannot be [[turing completeness|Turing complete]]. That means that there are computable functions that cannot be defined in the simply typed lambda calculus (and similarly there are computable functions that cannot be computed in the calculus of constructions or System F). As an example, it is impossible to define a [[self-interpreter]] in any of the calculi cited above.<ref>Conor McBride (May 2003), [http://www.haskell.org/pipermail/haskell-cafe/2003-May/004343.html "on termination"] (posted to the Haskell-Cafe mailing list).</ref>
==Coordinate-free definition==
The tautological 1-form can also be defined rather abstractly as a form on [[phase space]].  Let <math>Q</math> be a manifold and <math>M=T^*Q</math> be the [[cotangent bundle]] or [[phase space]]. Let
 
:<math>\pi:M\to Q</math>
 
be the canonical fiber bundle projection, and let
 
:<math>T_\pi:TM \to TQ </math>
 
be the [[Induced homomorphism|induced]] [[tangent map]].  Let ''m'' be a point on ''M''. Since ''M'' is the cotangent bundle, we can understand ''m'' to be a map of the tangent space at <math>q=\pi(m)</math>:
 
:<math>m:T_qQ \to \mathbb{R}</math>.
 
That is, we have that ''m'' is in the fiber of ''q''. The tautological one-form <math>\theta_m</math> at point ''m'' is then defined to be
 
:<math>\theta_m = m \circ T_\pi</math>.
 
It is a linear map
 
:<math>\theta_m:T_mM \to \mathbb{R}</math>
 
and so
 
:<math>\theta:M \to T^*M</math>.
 
==Properties==
The tautological one-form is the unique [[horizontal form|horizontal one-form]] that "cancels" a [[pullback_(differential geometry)|pullback]]. That is, let
 
:<math>\beta:Q\to T^*Q</math>
 
be any 1-form on ''Q'', and (considering it as a map from ''Q'' to ''T*Q'' ) let <math>\beta^*</math> be its pullback. Then
 
:<math>\beta^*\theta = \beta</math>,
 
which can be most easily understood in terms of coordinates:
 
:<math>\beta^*\theta = \beta^*(\sum_i p_i\, dq^i) =
\sum_i \beta^*p_i\,  dq^i = \sum_i \beta_i\, dq^i = \beta.</math>
 
So, by the commutation between the pull-back and the exterior derivative,
 
:<math>\beta^*\omega = -\beta^*d\theta = -d (\beta^*\theta) = -d\beta</math>.
 
==Action==
If ''H'' is a [[Hamiltonian mechanics|Hamiltonian]] on the [[cotangent bundle]] and <math>X_H</math> is its [[Hamiltonian flow]], then the corresponding [[action (physics)|action]] ''S'' is given by
 
:<math>S=\theta (X_H)</math>.
 
In more prosaic terms, the Hamiltonian flow represents the classical trajectory of a mechanical system obeying the [[Hamilton-Jacobi equations of motion]]. The Hamiltonian flow is the integral of the Hamiltonian vector field, and so one writes, using traditional notation for [[action-angle variables]]:
 
:<math>S(E) = \sum_i \oint p_i\,dq^i</math>
 
with the integral understood to be taken over the manifold defined by holding the energy <math>E</math> constant: <math>H=E=const.</math> .
 
==On metric spaces==
If the manifold ''Q'' has a Riemannian or pseudo-Riemannian [[Metric (mathematics)|metric]] ''g'', then corresponding definitions can be made in terms of [[generalized coordinates]].  Specifically, if we take the metric to be a map
 
:<math>g:TQ\to T^*Q</math>,
 
then define
 
:<math>\Theta = g^*\theta</math>
 
and
 
:<math>\Omega = -d\Theta = g^*\omega</math>
 
In generalized coordinates <math>(q^1,\ldots,q^n,\dot q^1,\ldots,\dot q^n)</math> on ''TQ'', one has
 
:<math>\Theta=\sum_{ij} g_{ij} \dot q^i dq^j</math>
 
and
 
:<math>\Omega= \sum_{ij} g_{ij} \; dq^i \wedge d\dot q^j +
\sum_{ijk} \frac{\partial g_{ij}}{\partial q^k} \;
\dot q^i\, dq^j \wedge dq^k</math>
 
The metric allows one to define a unit-radius sphere in <math>T^*Q</math>. The canonical one-form restricted to this sphere forms a [[contact structure]]; the contact structure may be used to generate the [[geodesic flow]] for this metric.


==See also==
==See also==
* [[Typed lambda calculus]]
* [[fundamental class]]
* [[Rewriting]]
* [[solder form]]
* [[Total functional programming]]
* [[Barendregt&ndash;Geuvers&ndash;Klop conjecture]]


==References==
==References==
{{Reflist}}
* [[Ralph Abraham]] and [[Jerrold E. Marsden]], ''Foundations of Mechanics'', (1978) Benjamin-Cummings, London ISBN 0-8053-0102-X ''See section 3.2''.


{{DEFAULTSORT:Normalization Property (Lambda-Calculus)}}
[[Category:Lambda calculus]]
[[Category:Logic in computer science]]


[[eo:Normaliga propraĵo (lambda-kalkulo)]]
[[Category:Symplectic geometry]]
[[zh:规范化性质]]
[[Category:Hamiltonian mechanics]]
[[Category:Lagrangian mechanics]]

Revision as of 03:21, 14 August 2014

In mathematics, the tautological one-form is a special 1-form defined on the cotangent bundle T*Q of a manifold Q. The exterior derivative of this form defines a symplectic form giving T*Q the structure of a symplectic manifold. The tautological one-form plays an important role in relating the formalism of Hamiltonian mechanics and Lagrangian mechanics. The tautological one-form is sometimes also called the Liouville one-form, the Poincaré one-form, the canonical one-form, or the symplectic potential. A similar object is the canonical vector field on the tangent bundle. In algebraic geometry and complex geometry the term "canonical" is discouraged, due to confusion with the canonical class, and the term "tautological" is preferred, as in tautological bundle.

In canonical coordinates, the tautological one-form is given by

Equivalently, any coordinates on phase space which preserve this structure for the canonical one-form, up to a total differential (exact form), may be called canonical coordinates; transformations between different canonical coordinate systems are known as canonical transformations.

The canonical symplectic form, also known as the Poincaré two-form, is given by

The extension of this concept to general fibre bundles is known as the solder form.

Coordinate-free definition

The tautological 1-form can also be defined rather abstractly as a form on phase space. Let be a manifold and be the cotangent bundle or phase space. Let

be the canonical fiber bundle projection, and let

be the induced tangent map. Let m be a point on M. Since M is the cotangent bundle, we can understand m to be a map of the tangent space at :

.

That is, we have that m is in the fiber of q. The tautological one-form at point m is then defined to be

.

It is a linear map

and so

.

Properties

The tautological one-form is the unique horizontal one-form that "cancels" a pullback. That is, let

be any 1-form on Q, and (considering it as a map from Q to T*Q ) let be its pullback. Then

,

which can be most easily understood in terms of coordinates:

So, by the commutation between the pull-back and the exterior derivative,

.

Action

If H is a Hamiltonian on the cotangent bundle and is its Hamiltonian flow, then the corresponding action S is given by

.

In more prosaic terms, the Hamiltonian flow represents the classical trajectory of a mechanical system obeying the Hamilton-Jacobi equations of motion. The Hamiltonian flow is the integral of the Hamiltonian vector field, and so one writes, using traditional notation for action-angle variables:

with the integral understood to be taken over the manifold defined by holding the energy constant: .

On metric spaces

If the manifold Q has a Riemannian or pseudo-Riemannian metric g, then corresponding definitions can be made in terms of generalized coordinates. Specifically, if we take the metric to be a map

,

then define

and

In generalized coordinates on TQ, one has

and

The metric allows one to define a unit-radius sphere in . The canonical one-form restricted to this sphere forms a contact structure; the contact structure may be used to generate the geodesic flow for this metric.

See also

References