<div dir="ltr"><div dir="auto"><div class="gmail_extra"><br><div class="gmail_quote">2017/09/29 午前0:09 "Martin Escardo" <<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.uk</a>>:<br type="attribution"><blockquote class="gmail-m_578991652899408436quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div class="gmail-m_578991652899408436elided-text"><br>
<br>
On 28/09/17 13:38, <a href="mailto:i.hidekazu@gmail.com" target="_blank">i.hidekazu@gmail.com</a> wrote:<br>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
Hello,<br>
<br>
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.<br>
<br>
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?<br>
</blockquote>
<br></div>
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).<br>
<br>
Here are two examples I remember without thinking too much:<br>
<br>
<br>
(1) Pour-el and Richards book, whose chapters are available individually on Project Euclid. <a href="https://www.google.com/search?client=ubuntu&hs=xgx&channel=fs&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.dummy_maps_web_fallback...0...1.1.64.psy-ab..0.1.94....0.xVYVMRJyYEc" rel="noreferrer" target="_blank">https://www.google.com/search?<wbr>client=ubuntu&hs=xgx&channel=f<wbr>s&q=pour-el+and+richards&oq=po<wbr>ur-el+and+richards&gs_l=psy-ab<wbr>.3..0i22i30k1l2.1396.1396.0.29<wbr>09.1.1.0.0.0.0.95.95.1.1.0.dum<wbr>my_maps_web_fallback...0...1.1<wbr>.64.psy-ab..0.1.94....0.xVYVMR<wbr>JyYEc</a><br>
<br>
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.<br>
<br>
(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.<br>
<a href="http://homepages.inf.ed.ac.uk/jrl/Research/laplace1.pdf" rel="noreferrer" target="_blank">http://homepages.inf.ed.ac.uk/<wbr>jrl/Research/laplace1.pdf</a></blockquote><div class="gmail_quote"><span style="font-size:14px">Bas Spitters wrote:</span></div><div class="gmail_quote"><span style="font-size:14px">>Regarding the wave equation you may want to read:</span><br style="font-size:14px"><span style="font-size:14px">>The Wave Propagator Is Turing Computable</span><br style="font-size:14px">><a href="https://link.springer.com/content/pdf/10.1007/3-540-48523-6_66.pdf" rel="noreferrer" target="_blank" style="font-size:14px">https://link.springer.com/<wbr>content/pdf/10.1007/3-540-<wbr>48523-6_66.pdf</a><br></div><div class="gmail_quote"><br></div><div class="gmail_quote">Thank you for your presentation of the references! I'm really grateful to give answer!</div><div class="gmail_quote">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. </div><div class="gmail_quote"><br></div><div class="gmail_quote">Frankly speaking, I want to get interpretations of "type" of typed value in knowledge about physics.(not physical interpretation)</div><div class="gmail_quote"><br></div><div class="gmail_quote">Although it is not systematic enough, I think that Lajas Yánossy's representation theory on physical reality includes any hints, probably.</div><div class="gmail_quote">(His theory is written in "Theory of relativity based on physical reality". <a href="https://www.amazon.com/dp/0569066336">https://www.amazon.com/dp/0569066336</a> But I have only the Japanese version.)</div><div class="gmail_quote">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</div><div class="gmail_quote"> R(α) = a</div><div class="gmail_quote">that is to say,</div><div class="gmail_quote"> R(<a physical reality>) = <its measure>.</div><div class="gmail_quote">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</div><div class="gmail_quote"> a : α,</div><div class="gmail_quote"> <its measure> : <a physical reality>.</div><div class="gmail_quote">Therefore, we think that the consideration of relationships between physical realities corresponds the type inference.</div><div class="gmail_quote"><br></div><div class="gmail_quote">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.</div><div class="gmail_quote"><br></div><div class="gmail_quote">The difficulties, it goes without saying, are clear to all.</div><div class="gmail_quote"><br></div><div class="gmail_quote">So, I'd like to ask for information on typed physical language system or interpretations of typed value.</div><div class="gmail_quote">If it's possible, it would be good that anyone provides any ideas about the above topic.</div><div class="gmail_quote"><br></div><div class="gmail_quote">Sincerely,</div><div class="gmail_quote">IWAKI</div><div class="gmail_quote"><br></div><blockquote class="gmail-m_578991652899408436quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
Martin<br>
<br>
<br>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
sincerely,<br>
<br>
IWAKI Hidekazu<br>
<br>
<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
<br><font color="#888888">
</font></blockquote><font color="#888888">
<br>
-- <br>
Martin Escardo<br>
<a href="http://www.cs.bham.ac.uk/~mhe" rel="noreferrer" target="_blank">http://www.cs.bham.ac.uk/~mhe</a><br>
</font></blockquote></div><br></div></div>
</div>