Automatic proofs or model checking in an extremely simplified functional language

Question

Imagine a stripped down functional programming language, that has the following properties

• The only value type is an integer
• There are no side effects
• Functions are defined as a single expression, value of which becomes the return value of the function.
• Program consists of zero or more function definitions and an expression. The expression can be defined in terms of the previously defined functions. Value of that evaluated expression is the result of the program.
• Aside from simple arithmetic, there is only an if then else fi expression
• The only way to do looping is through recursion

A program can then look like

f(x) = r(x+1,1)
r(x,y) = if x-(y*y) then r(x,y+1) else y*y fi

f(2)

so f() computes the second power of the given argument.

My question is, whether it is possible with current automated tools to prove theorems about such programs without human assistance. And what exactly?

Is it for example possible to automatically say for sure that for two functions f and g for every x: f(x) = g(x) ?

Answer 1

The ACL2 system includes all of the features of your language, and supports impressive automated theorem proving about program in that language.

In ACL2, you would write the theorem you describe as:

(defthm f-g-equal (equal (f x) (g x)))

having previously defined f and g.

Answer 2

The general area of study you're talking about is called automated theorem proving.

I think that there are two things you should look at. One is SMT solvers (http://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories). The SMT problem is an extension of SAT (the question of whether a boolean formula is satisfiable or not) with a background theory (e.g. integers.) There are many SMT solvers out there to play with, but I suggest Yices as it's really easy to use. Look into things that use SMT-LIB if you get serious about this.

The other thing you'd be interested in is how propositions can be represented. In intuitionistic type theory and all of the languages based on it (Coq, Agda, etc.) both types like your integers and propositions are represented as types. I think you'll want to take a look at an Agda tutorial to get an idea of what that looks like. Anyhow, proof search in these systems is not decidable, in general. However systems like Coq (and the newer more programming-oriented Idris) support "tactics", which are scripts that allow one to direct proof search.

To answer your question more directly, it really depends on exactly what you're trying to prove. If the proposition that you're trying to prove is indeed false, there's no guarantee that the automated theorem prover will terminate as per Gödel's incompleteness theorem. If the proposition is true, you will eventually get a proof back, but depending on what you have in your underlying theory the complexity of doing so will vary. I believe there are many efficient algorithms for integers and booleans.

Regarding the last part of your question. One solution to that problem is called "observational equality."

Answer 3

Your language would be crippled for these reasons:

• It has no aggregate data structures, making compositions impossible

• It is not optimally minimalistic: You should consider integrating the lambda calculus to your language from which you can derive numbers and conditionals among other constructs

• A program defined as 0 or more definitions does not return; you can define programs as the application of values on anonymous function arguments, so that programs are applied closures, and definitions could then be represented as the binding of a function's arguments to the values returned by the enclosing environment (just before arguments get applied, they are bound to their corresponding values)

You should definitively learn Scheme...