[Agda] Can intuitionistic type theory express derivations of physical equations more strictly?

[Hidekazu IWAKI]

2017/09/29 午前0:09 "Martin Escardo" <m.escardo at cs.bham.ac.uk>:



On 28/09/17 13:38, i.hidekazu at gmail.com wrote:

> Hello,
>
> 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

Bas Spitters wrote:
>Regarding the wave equation you may want to read:
>The 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,
>
> IWAKI Hidekazu
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170929/3f4b7226/attachment.html>