Post by Hidekazu IWAKIHello,
I'd like to describe a physical system with the intuitionistic type
theory(not computer simulation). I wonder if it is possible to convince
readers that all famous physical equations have evenly a strict derivation.
So I want to confirm it with the type theory.
In order to refer, I'm looking about such a system, a plot or a
interpretation of value with type in physics. Does anyone know such a
information?
I don't know about your question with intuitionistic mathematics. But
people have thought about this in the context of computability theory
(developed within classical mathematics, as usual - which is closely
related, as well as closely unrelated to intuitionistic mathematics).
Here are two examples I remember without thinking too much:
(1) Pour-el and Richards book, whose chapters are available individually on
Project Euclid. https://www.google.com/search?client=ubuntu&hs=xgx&channel=f
s&q=pour-el+and+richards&oq=pour-el+and+richards&gs_l=psy-ab
.3..0i22i30k1l2.1396.1396.0.2909.1.1.0.0.0.0.95.95.1.1.0.dum
my_maps_web_fallback...0...1.1.64.psy-ab..0.1.94....0.xVYVMRJyYEc
There the heat and wave (differential) equations are discussed. For one of
them, the solution is computable from the initial condition. For the other
one, it isn't.
(2) John Longley, University of Edinburgh, On the calculating power of
Laplace's demon (Part I). I don't think part II exists in writing. This is
an extended version of a CiE'2006 publication.
http://homepages.inf.ed.ac.uk/jrl/Research/laplace1.pdf
Post by Hidekazu IWAKIThe Wave Propagator Is Turing Computable
https://link.springer.com/content/pdf/10.1007/3-540-48523-6_66.pdf
Thank you for your presentation of the references! I'm really grateful to
give answer!
As you have said, I'd like to construct computability theory of physics, if
it's possible. But I'm not quite advanced enough yet, just thinking basic
design.
Frankly speaking, I want to get interpretations of "type" of typed value in
knowledge about physics.(not physical interpretation)
Although it is not systematic enough, I think that Lajas Yánossy's
representation theory on physical reality includes any hints, probably.
(His theory is written in "Theory of relativity based on physical reality".
https://www.amazon.com/dp/0569066336 But I have only the Japanese version.)
In the book, physical reality and its measure are distinguished. A physical
measure "a" is a representation of physical reality "α" to show an aspect
of α. He formed this relationship between a reality and its measure by
representation function R to grasp an aspect of the reality
R(α) = a
that is to say,
R(<a physical reality>) = <its measure>.
I realize that it perhaps opens up a little possibility to interpreting
physical reality as type. In other words, above relationship can be rewrite
to
a : α,
<its measure> : <a physical reality>.
Therefore, we think that the consideration of relationships between
physical realities corresponds the type inference.
To tell the truth, I thought it was nice idea; however, Yánossy's physical
realism is not systematic and ambiguous. If I went this approach, I must
rebuild his physical realism to match the intuitionistic type theory.
The difficulties, it goes without saying, are clear to all.
So, I'd like to ask for information on typed physical language system or
interpretations of typed value.
If it's possible, it would be good that anyone provides any ideas about the
above topic.
Sincerely,
IWAKI
Martin
sincerely,
Post by Hidekazu IWAKIIWAKI Hidekazu
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
--
Martin Escardo
http://www.cs.bham.ac.uk/~mhe