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

<p>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.</p>

<p>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.</p>

<p>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. </p>

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

CC BY-SA 3.0
2012-02-11T22:19:23.163Z
2012-02-11T22:19:23.163Z
Anthony
<p>Your language would be crippled for these reasons:</p>

<ul>
<li><p>It has no aggregate data structures, making compositions impossible</p></li>
<li><p>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</p></li>
<li><p>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)</p></li>
</ul>

<p>You should definitively learn Scheme...</p>

CC BY-SA 3.0
2012-01-28T05:43:12.053Z
This recommendation to improve an intentionally simple language is not an answer to the question posed.
jbapple
CC BY-SA 3.0
2012-02-11T22:05:12.013Z
This is not only not an answer, but also rather misleading. The recommendation to learn scheme is also not relevant.
Anthony
CC BY-SA 3.0
2012-01-27T18:25:05.173Z
2012-01-27T18:25:05.173Z
Samuel Duclos
<p>The <a href="http://www.cs.utexas.edu/~moore/acl2/">ACL2 system</a> includes all of the features of your language, and supports impressive automated theorem proving about program in that language.</p>

<p>In ACL2, you would write the theorem you describe as:</p>

<pre><code>(defthm f-g-equal (equal (f x) (g x)))
</code></pre>

<p>having previously defined <code>f</code> and <code>g</code>.</p>

CC BY-SA 3.0
2012-02-11T22:58:39.703Z
@Anthony: I wasn't attempting to give a comprehensive overview of theorem-proving tools, but rather an proof by example that what the question asked for is possible.
Sam Tobin-Hochstadt
CC BY-SA 3.0
2012-02-11T23:00:32.243Z
Also, I think ACL2 is probably the most widely used automated theorem prover for a rich language.  Certainly SAT/SMT tools are also widely used, but they wouldn't support the systems the question asked about.
Sam Tobin-Hochstadt
CC BY-SA 3.0
2012-01-27T19:43:50.110Z
2012-01-27T19:43:50.110Z
Sam Tobin-Hochstadt
<p>Imagine a stripped down functional programming language, that has the following properties</p>

<ul>
<li>The only value type is an integer</li>
<li>There are no side effects</li>
<li>Functions are defined as a single expression, value of which becomes the return value of the function.</li>
<li>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.</li>
<li>Aside from simple arithmetic, there is only an if then else fi expression</li>
<li>The only way to do looping is through recursion</li>
</ul>

<p>A program can then look like</p>

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

f(2)
</code></pre>

<p>so <code>f()</code> computes the second power of the given argument.</p>

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

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

CC BY-SA 3.0
2012-02-12T14:49:40.150Z
Your language is commonly known as PCF, see http://en.wikipedia.org/wiki/Programming_Computable_Functions. It is Turing complete so there is no chance that its theory were decidable.
Andrej Bauer
<lo.logic><pl.programming-languages><functional-programming><automated-theorem-proving>
Automatic proofs or model checking in an extremely simplified functional language
user7610
# Automatic proofs or model checking in an extremely simplified functional language

(Asked by: username_0 on 2012-01-27)

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) ?

**Tags:** lo.logic, pl.programming-languages, functional-programming, automated-theorem-proving

> **Comments:**
> **username_1**: Your language is commonly known as PCF, see http://en.wikipedia.org/wiki/Programming_Computable_Functions. It is Turing complete so there is no chance that its theory were decidable.  

---

## 3 answers

### Answer by username_5 on 2012-01-27. Score: 8 | Accepted answer

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.

> **Comments:**
> **username_5**: @username_2: I wasn't attempting to give a comprehensive overview of theorem-proving tools, but rather an proof by example that what the question asked for is possible.  
> **username_5**: Also, I think ACL2 is probably the most widely used automated theorem prover for a rich language.  Certainly SAT/SMT tools are also widely used, but they wouldn't support the systems the question asked about.  

---

### Answer by username_2 on 2012-02-11. Score: 3

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 by username_3 on 2012-01-27. Score: -6

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...

> **Comments:**
> **username_4**: This recommendation to improve an intentionally simple language is not an answer to the question posed.  
> **username_2**: This is not only not an answer, but also rather misleading. The recommendation to learn scheme is also not relevant.  

---

