Proposed terminological change: Replace “Inductive Type” with “Free Type”

The elimination axiom for natural numbers, surreal numbers, lists, and trees can all be properly called induction. However, I don’t think the expression if b then x else y is an example of recursion, and so I don’t think 2 should be called an inductive type. Similarly, I don’t like how the term inductive type is used for dependent sums, unit and null types, and the various new types of homotopy type theory. What all these types share in common is that they have a set of constructors and an elimination axiom which essentially says that these constructors are the only way to obtain an element of these types. A better terminology would be such a type is the free type over a set of
constructors, and to call such a type a free type.

A Small Insight on Quantum Field Theory

I’ve been thinking about quantum field theory for a while now, trying to
understand it.. Here is a small insight I recently made.

One way of thinking about the configuration space is through the field
perspective. There are observables at every point in space, they obey the
Klein-Gordon equation with nonlinear perturbations. Taking the Fourier
transform, you get at every momentum a set of harmonic oscillators, and the
interactions are couplings between them. Quantizing this, each oscillator gets
an integer spectrum which corresponds to how many particles of a given type
there is in a given momentum. So now we get the particle perspective in momentum

Another perspective, which is usually used in less rigorous descriptions of QFT,
is the particle presentation in position space. For example, this is implicit
in the “cloud of virtual particles” intuition. It seems to work, but nobody uses
it in calculation. Presumably it can described precisely by taking the Fourier
transform of the momentum space particles to get position space particles. Like
the field presentation, it seems to be manifestly local.

My small insight is this: there is a direct way to describe this perspective in
terms of the field perspective. It is this: a field at a given point over time
behaves somewhat like a harmonic oscillator. Take the basis derived from the
fixed energy states of these harmonic oscillators to get position-space particle

Some consequences:

  • A massless field doesn’t behave like a harmonic oscillator at a fixed position because there is no spring constant. This explains a claim I heard that position
    space doesn’t work for massless particles. However, extrapolating the creation
    operator as the spring consant goes to zero, it looks like something similar can
    be made to work when thinking of particle count as an index for a
    Taylor-expansion-like decomposition of the wavefunction into polynomials.
  • This position space perspective is not Lorenz-invariant. This partially
    explains the claim I heard that position space also doesn’t work for massive
    particles in the relativistic theory. It also explains why nobody uses this
    perspective seriously.