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

[Bas Spitters]

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

On Thu, Sep 28, 2017 at 5:09 PM, Martin Escardo <m.escardo at cs.bham.ac.uk> wrote:
>
>
> 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=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
>
> 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
>
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda