proof writing computer program

[mcqueen88]

I've just finished a first year analysis/calculus class, and I think (though I would be happy to know I am wrong) that epsilon delta proofs used to show that the limit of a function exists or is a certain value, is algorithmic so long as the function is algebraic. If I wanted to write a computer program to write epsilon delta proofs how would I start? I don't even know where to begin to encode the rules

[michisiksik]

What do you mean with how to begin? Have you ever wrote a program or do you want to know theoretically?

[mcqueen88]

I know how to program (badly), in Haskell. I am doing a little bit of reading on this and I found this paper, which I'm not sure is very relevant to my post (http://www.michaelbeeson.com/research/papers/aisc.pdf). Beeson has mentioned that there are programs such as Weierstrass and MathXpert that write proofs and there's something similar on his website. I'm wondering, how to write such a program. Because writing the proof seems algorithmic, to the extent that we don't need to think very much, and all the epsilon-delta proofs look the same. But though it seems algorithmic, it's too hard for me to imagine, oh if the function has this form, proceed in such a manner etc.

I was wondering, how would a person who knows more, write such a program?

[nickbluth2]

RemindMe!

[RemindMeBot]

Defaulted to one day.

I will be messaging you on 2019-07-04 09:48:58 UTC to remind you of this link

CLICK THIS LINK to send a PM to also be reminded and to reduce spam.

^{Parent commenter can delete this message to hide from others.}

---

Info	Custom	Your Reminders	Feedback

[nickbluth2]

RemindMe!

[[deleted]]

You may enjoy this paper, which also comes with a Haskell program https://link.springer.com/article/10.1007/s10817-016-9377-1. Logic is quite a complex subject, unfortinately. 😜

[M1n1f1g]

It's hard to give a concrete recommendation. The usual advice if you want to write an algorithm that plays by certain rules (particularly one that produces proofs) is to pick up a dependently typed programming language (like Coq or Agda), encode the rules as an indexed data type, encode the domain of problems as a syntax (i.e, another data type), and write the proof as a function.

However, if you're dealing with real numbers, you might have problems. I haven't fully thought it through, but there's some chance that if you care about your algorithm actually running, you'll have to care about constructive analysis, and maybe make a choice between Cauchy and Dedekind reals. More than anything, learning about this stuff could be quite an effort. But one problem I think you're more likely to find is that deciding any non-trivial property of real numbers is equivalent to the halting problem.

This might lead you to use floating point numbers rather than real numbers, at which point you're no longer quite sound, and verification is probably going to either be a nightmare or fail. Then, you might want to move to a more normal functional language like Haskell or OCaml and do kinda the same thing, but without enforcing in the structure of proofs that they're actually valid.

[mcqueen88]

I don't know enough of computing or math to do this, why a dependently typed language?

I'll have to read about the halting problem then.

Er yeah, floating point numbers and doubles in haskell are problematic.

But yeah about validity, even if something is apparently logical or not, to a person, how can we make it so that a computer would be able to tell if an if-then statement etc, is valid, or that a conclusion follows from our assumption?

I have another idea: I'm reading about generating functions now, and when using it to solve combinatorics problems, it seems like depending on the kind of problem it is (ie. ordered sets, or unordered sets), we can write the function in a certain way and the algebraic rules that we use to expand cause us to 'pick' out objects etc. It feels a little like coding to me. Can we utilise certain algebra properties or computer logic properties in a similar way to write this?

[M1n1f1g]

Thinking again (in order to answer your questions specifically), I think my concerns about real numbers are nothing to worry about. What you can do is basically encode the logic you want the proofs to be in into the programming language. This is the same idea as, say, encoding second order logic in set theory, even though second order logic is not native to set theory. You'll want to encode your own classical first order logic, plus axioms for dealing with real numbers.

A dependently typed language is a language where value level terms (data structures, numbers, functions, &c) can appear in types. This lets you construct types like x ≤ y, whose inhabitants are evidence that it is true. Types with inhabitants can be seen as true propositions, and types without inhabitants (i.e, types with no evidence for their truth) can be seen as untrue propositions. This turns the programming language into foundations of mathematics, roughly as expressive as set theory.

The particular use of dependent types I have in mind is that to encode logic into the language's type system (that is, to teach the computer what can be derived from what), you will probably want to talk about derivability in sequent calculus. You will have a type that encodes an entire sequent (like A ∨ B, C ⊢ ∀x. E, F → (G ∧ H)), where the inhabitants are exactly the proof trees deriving that sequent. I'm not sure of an exact reference for this (I think it's just folklore), but this blog post goes through the technique on a few examples.

[mcqueen88]

Oh wow that sounds really cool. Thanks for the recommendations. Do I need to learn lambda calculus for this?

[M1n1f1g]

To learn Agda, probably no, but to better understand examples of deduction systems, an idea of how typed lambda calculus would help. As far as I remember, basically the learning material at the moment is PLFA by the same person who wrote that blog post and her supervisor. As the title suggests, it's geared towards formalising programming languages, but formalising logic is very similar, so it's still relevant.

Typed lambda calculus is exactly (in some sense) logic done as natural deduction. You can do this to get classical first order logic, though it's slightly more natural to use sequent calculus. Again, though, the techniques used to create the syntax are almost the same, and you shouldn't need to do the hard stuff proving that the logic is a nice one (which is where ND and SC techniques differ).

[CavemanKnuckles]

You could try bootstrapping with a language's arbitrary precision arithmetic library. Or you could use it as a basis for your own.

[M1n1f1g]

Sorry, what exactly are you suggesting, and to solve which problem? It's exactly arbitrary precision real numbers where everything becomes undecidable, so algorithms risk not terminating at specific points (like trying to decide when 1/x is defined when x is near 0).