Home » forums » LtU Forum

Combining Theorem Proving and Programming

Just as there's been work by Connor Mcbride on Epigram, there has been work by Hongwei Xi on ATS (previously mentioned on LTU). In one of his most recent papers, to appear at ICFP 05, a type system for a language which includes proof development facilities in the type system is presented . This work has an advantage of his previous work with DML in that type system is more expressive.

By carter at 2005-09-07 15:16 | LtU Forum | previous forum topic | next forum topic | other blogs | 7443 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Type enforced conservation laws

Lately I've been wondering if anyone has been using a type system to enforce conservation laws. For example, a bank might be interested in knowing that their software system conserves dollars (neither destroying or creating them). And of course physics simulations might be a popular target. Where we would like to ensure that our algorithms conserve energy, or momentum, or charge. I've got the vague feeling that linear or unique types (is there a difference?) might be helpful here. Any pointers?

By Greg Buchholz at Wed, 2005-09-07 15:41 | login or register to post comments

Noether's theorem

You should be able to prove conservation by symmetry Noether style, e.g. All dollar handling functions are isomorphisms. Whether you can prove an isomorphism directly in any of the above mentioned systems I don't know.

By Daniel Slaney at Thu, 2005-09-08 07:52 | login or register to post comments

Linear types plus Xi's DML...

...would get you basically what you're talking about.

What you want are linear or unique values, which have a DML index. I'll write Lin(t) for a linear reference to a type t.

I'll also write t(n) for a type indexed by a DML index. What you want is an abstract type for money with an interface that looks like:

val split : forall n. forall m. n  (Lin(money(m)) -> (Lin(money(n)) * Lin(money(m - n)))

Now, if your money interface conserves money, you can take apart piles of money and then do stuff with them, and at the end of the day your program has to return the same stuff as it took in.

Basically, this says that if you have money m, then you can split it into two pieces of money n and (m-n) and use them both separately (and linearly).

Also, this reminds me of fractional permissions for some reason.

By neelk at Fri, 2005-09-09 17:25 | login or register to post comments

DML?

DML is Dependent ML I presume.

By Greg Buchholz at Fri, 2005-09-09 19:56 | login or register to post comments

Right -- I just assumed that

Right -- I just assumed that since that abbreviation was used in the article, I could mention it in a reply.

By neelk at Fri, 2005-09-09 22:32 | login or register to post comments

Noether

I assume you mean this Noether's theorem. Very interesting. My physics knowledge didn't extend that far, so I'll be carefully studying it. Thanks.

By Greg Buchholz at Thu, 2005-09-08 15:12 | login or register to post comments

Yes, that one.

All I really know about it is 'symmetries imply conservation laws' and the main example of 'time symmetry implies conservation of energy'. With all work about differentiating data types and so on recently it might actually have a direct application.

I've had an idea on the back burner for a while about trying to see if this theorem can be generalised and applied to computational semantics. Time symmetric (invertible) programs would seem intuitively to conserve some kind of information as an allegory to energy.

Not sure how a Hamiltonian can be applied to prog' semantics though |:^)

By Daniel Slaney at Fri, 2005-09-09 08:02 | login or register to post comments

iirc there's work on the cost

iirc there's work on the cost of changing state (flipping a bit). think of the connection between information and entropy. if i remember more, or can dig something out of google, i'll post again. i think something was once posted here (old site).

By andrew cooke at Fri, 2005-09-09 19:28 | login or register to post comments

kln(2)

This is an important and basic result. For some context, and links to current research, look here.

By Ehud Lamm at Fri, 2005-09-09 20:06 | login or register to post comments

Combining Theorem Proving and XXX

You might also be interested in some of the work on MathScheme which aims to combine theorem proving and computer algebra at a very fundamental level. The Focal Project also combines (certified) computer algebra and theorem proving in interesting (but orthogonal) ways to MathScheme. This works fits well within the confines of the (now defunct) Calculemus Project.

The MAP project is more ambitious still, trying to unite computer algebra, constructive algebra and proof systems. Of course, via Curry-Howard, that's just programming in another guise. Admitedly, some large-scale experiments in program extraction yielded very mixed results [Nota Bene: the paper linked was awarded "Best Paper" at Calculemus 2005].

By Jacques Carette at Fri, 2005-09-09 01:28 | login or register to post comments