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

[Martin Escardo]

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