29 07 2008

## Intro

In this semester had to do this project with my friend, João Moura, under supervision of professor Alcino Cunha.

The project was to make a program that make automatic the process of proving an equality of functions written in the pointfree style. Not completely automatic, but so iterative. The program load a file with rules and the user inserts an equality of functions in pointfree and can surf the words to find a sub-expression which want to run a particular rule. From the side are shown all the rules that may apply to selected sub-expression.

## What is pointfree?

Pointfree is a style of programming that helps us to compose functions. Even more, it helps us later to prove equality between functions.

How can someone prove equality between functions? We can do so, because we have rules. Let’s see an analogy with algebraic calculus.

$\noindent (a + b) + c + d \times 0 = a + (b + c)$
$\noindent \Leftrightarrow \textrm{\{Neutral element of the multiplication\}}$
$\noindent (a + b) + c + 0 = a + (b + c)$
$\noindent \Leftrightarrow \textrm{\{Neutral element of addition\}}$
$\noindent (a + b) + c = a + (b + c)$
$\noindent \Leftrightarrow \textrm{\{Associativity of addition\}}$
$\noindent a + (b + c) = a + (b + c)$

We have proved that $\noindent (a + b) + c + d \times 0 = a + (b + c)$.

Pointfree calculus as is done now, on paper, is boring and repetitive. A proof is this image of someone trying to make a proof.

## Abstract representation

If swap is a functions for exchange the elements of a pair:

swap (a,b) = (b,a) --in pointwise
swap = split snd fst --in pointfree

And we want to prove that: $f \circ swap \circ swap = f$. This is clearly obvious, but I will use this example just to show you the representation that we use to see these proofs.

So, here we have the representation of $f \circ swap \circ swap = f$:

$\xymatrix @!=.5pc { & & & = \ar@/^/[lld] \ar@/^/[rrd] & & \\& \circ \ar@/^/[d] \ar@/^/[ld] \ar@/^/[rd] & & & & f \\f & swap & swap & & & \\}$

If you make a inorder passage it make sense.

As you can see the $\circ$ operator have arity n. Because we want that this operator became flat, we never want to use the $assoc~\circ$ law:
$(f \circ g) \circ h = f \circ (g \circ h)$.

Function f is variable, and swap is constant, we know their definition.

Imagine now that we load the following file of rules:

$swap = snd \Delta fst$
$(g \Delta h) \circ f = g \circ f \Delta h \circ f$
$fst \circ (f \Delta g) = f, snd \circ (f \Delta g) = g$
$fst \Delta snd = id$
$f \circ id = f = id \circ f$

## Path

In order to know that sub-expression are to select a term, we have the Path which behaves as follows:

If we select 4 in the following expression $1+(2*(3/4))$, the Path becomes: $/1/1/1/[]$.
If we select 2, the Path becomes: $/1/0/[]$.

the list in front of the Path is to select a range of elements in an operator with arity n. Thus, if we want select $swap \circ swap$ in $f \circ swap \circ swap = f$, the Path becomes: $/0/[1,2]$.

## Proof of $f \circ swap \circ swap = f$

This process is pretty always the same, but I suggest that you follow with some attention.

$\xymatrix @!=.5pc { & & & = \ar@2{~>}[lld] \ar@/^/[rrd] & & \\& \circ \ar@2{~>}[d] \ar@/^/[ld] \ar@/^/[rd] & & & & f \\f & swap & swap & && \\}$

In this first tree I will show the Path already selected.

Here I will show the rule that will apply in our expression, and the instantiation of that rule to our selected sub-expression.

• Selected function: $swap$
• Path: $/0/1/[]$
• Rule: $swap = snd \Delta fst$
• Instantiation of the rule: $snd \Delta fst$

So, the resulting tree will be:

$\xymatrix @!=.5pc { & & & = \ar@/^/[lld] \ar@/^/[rrd] & & \\& \circ \ar@/^/[d] \ar@/^/[ld] \ar@/^/[rd] & & & & f \\f & \Delta \ar@/^/[dr]\ar@/^/[dl] & swap & & & \\snd & & fst & & & \\}$

Resulting function: $f \circ (snd \Delta fst) \circ swap = f$.

### Proof of $f \circ (snd \Delta fst) \circ swap = f$

$\xymatrix @!=.5pc { & & & = \ar@2{~>}[lld] \ar@/^/[rrd] & & \\& \circ \ar@{.>}[d] \ar@/^/[ld] \ar@{.>}[rd] & & & & f \\f & \Delta \ar@/^/[dr] \ar@/^/[dl] & swap & & & \\snd & & fst & & & \\}$

• Selected function: $(snd \Delta fst) \circ swap$
• Path: $/0/[1,2]$
• Rule: $(g \Delta h) \circ f = g \circ f \Delta h \circ f$
• Instantiation of the rule: $snd \circ swap \Delta fst \circ swap$

So, the resulting tree will be:

$\xymatrix @!=.5pc { & & & = \ar@/^/[dl] \ar@/^/[dr] & & \\& & \circ \ar@/^/[dl] \ar@/^/[dr] & & f & \\& f & &\Delta \ar@/^/[dll] \ar@/^/[dr] & & \\& \circ \ar@/^/[dl] \ar@/^/[dr] & & & \circ \ar@/^/[dl] \ar@/^/[dr]& \\snd & & swap & fst & & swap \\}$

Resulting function: $f \circ (snd \circ swap \Delta fst \circ swap) = f$.

### Proof of $f \circ (snd \circ swap \Delta fst \circ swap) = f$

$\xymatrix @=.5pc { & & & = \ar@2{~>}[dl] \ar@/^/[dr] & & \\& & \circ \ar@/^/[dl] \ar@2{~>}[dr] & & f & \\& f & &\Delta \ar@2{~>}[dll] \ar@/^/[dr] & & \\& \circ \ar@/^/[dl] \ar@2{~>}[dr] & & & \circ \ar@/^/[dl] \ar@/^/[dr]& \\snd & & swap & fst & & swap \\}$

• Selected function: $swap$
• Path: $/0/1/0/1/[]$
• Rule: $swap = snd \Delta fst$
• Instantiation of the rule: $snd \Delta fst$

So, the resulting tree will be:

$\xymatrix @!=.5pc { & & & = \ar@/^/[dl] \ar@/^/[dr] & & \\& & \circ \ar@/^/[dl] \ar@/^/[dr] & & f & \\& f & &\Delta \ar@/^/[dll] \ar@/^/[dr] & & \\& \circ \ar@/^/[dl] \ar@/^/[dr] & & & \circ \ar@/^/[dl] \ar@/^/[dr]& \\snd & & \Delta \ar@/^/[dl] \ar@/^/[dr] & fst & & swap \\& snd&& fst& & \\}$

Resulting function: $f \circ (snd \circ (snd \Delta fst) \Delta fst \circ swap) = f$.

### Proof of $f \circ (snd \circ (snd \Delta fst) \Delta fst \circ swap) = f$

$\xymatrix @=.5pc { & & & = \ar@2{~>}[dl] \ar@/^/[dr] & & \\& & \circ \ar@/^/[dl] \ar@2{~>}[dr] & & f & \\& f & &\Delta \ar@2{~>}[dll] \ar@/^/[dr] & & \\& \circ \ar@/^/[dl] \ar@/^/[dr] & & & \circ \ar@/^/[dl] \ar@/^/[dr]& \\snd & & \Delta \ar@/^/[dl] \ar@/^/[dr] & fst & & swap \\& snd&& fst& & \\}$

• Selected function: $snd \circ (snd \Delta fst)$
• Path: $/0/1/0/[]$
• Rule: $snd \circ (f \Delta g) = g$
• Instantiation of the rule: $fst$

So, the resulting tree will be:

$\xymatrix @!=.5pc { & & & = \ar@/^/[dl] \ar@/^/[dr] & & \\& & \circ \ar@/^/[dl] \ar@/^/[dr] & & f & \\& f & &\Delta \ar@/^/[dl] \ar@/^/[dr] & & \\& & fst& & \circ \ar@/^/[dl] \ar@/^/[dr]& \\& & & fst & & swap \\}$

Resulting function: $f \circ (fst \Delta fst \circ swap) = f$.

### Proof of $f \circ (fst \Delta fst \circ swap) = f$

$\xymatrix @=.5pc { & & & = \ar@2{~>}[dl] \ar@/^/[dr] & & \\& & \circ \ar@/^/[dl] \ar@2{~>}[dr] & & f & \\& f & &\Delta \ar@/^/[dl] \ar@2{~>}[dr] & & \\& & fst& & \circ \ar@/^/[dl] \ar@2{~>}[dr]& \\& & & fst & & swap \\}$

• Selected function: $swap$
• Path: $/0/1/1/1/[]$
• Rule: $swap = snd \Delta fst$
• Instantiation of the rule: $snd \Delta fst$

So, the resulting tree will be:

$\xymatrix @!=.5pc { & & & = \ar@/^/[dl] \ar@/^/[dr] & & &\\& & \circ \ar@/^/[dl] \ar@/^/[dr] & & f & &\\& f & &\Delta \ar@/^/[dl] \ar@/^/[dr] & & &\\& & fst& & \circ \ar@/^/[dl] \ar@/^/[dr]& &\\& & & fst & & \Delta \ar@/^/[dl] \ar@/^/[dr] &\\& & & & snd& & fst\\}$

Resulting function: $f \circ (fst \Delta fst \circ (snd \Delta fst)) = f$.

### Proof of $f \circ (fst \Delta fst \circ (snd \Delta fst)) = f$

$\xymatrix @=.5pc { & & & = \ar@2{~>}[dl] \ar@/^/[dr] & & &\\& & \circ \ar@/^/[dl] \ar@2{~>}[dr] & & f & &\\& f & &\Delta \ar@/^/[dl] \ar@2{~>}[dr] & & &\\& & fst& & \circ \ar@/^/[dl] \ar@/^/[dr]& &\\& & & fst & & \Delta \ar@/^/[dl] \ar@/^/[dr] &\\& & & & snd& & fst\\}$

• Selected function: $fst \circ (snd \Delta fst)$
• Path: $/0/1/1/[]$
• Rule: $fst \circ (f \Delta g) = f$
• Instantiation of the rule: $snd$

So, the resulting tree will be:

$\xymatrix @!=.5pc { & & = \ar@/^/[dl] \ar@/^/[dr]& \\& \circ \ar@/^/[dl] \ar@/^/[dr]& & f \\f & & \Delta \ar@/^/[dl] \ar@/^/[dr]& \\& fst & & snd \\}$

Resulting function: $f \circ (fst \Delta snd) = f$.

### Proof of $f \circ (fst \Delta snd) = f$

$\xymatrix @!=.1pc { & & = \ar@2{~>}[dl] \ar@/^/[dr]& \\& \circ \ar@/^/[dl] \ar@2{~>}[dr]& & f \\f & & \Delta \ar@/^/[dl] \ar@/^/[dr]& \\& fst & & snd \\}$

• Selected function: $fst \Delta snd$
• Path: $/0/1/[]$
• Rule: $fst \Delta snd = id$
• Instantiation of the rule: $id$

So, the resulting tree will be:

$\xymatrix @!=.1pc { & & = \ar@/^/[dl] \ar@/^/[dr]& \\& \circ \ar@/^/[dl] \ar@/^/[dr]& & f \\f & & id & \\}$

Resulting function: $f \circ id = f$.

### Proof of $f \circ id = f$

$\xymatrix @!=.1pc { & & = \ar@2{~>}[dl] \ar@/^/[dr]& \\& \circ \ar@/^/[dl] \ar@/^/[dr]& & f \\f & & id & \\}$

• Selected function: $f \circ id$
• Path: $/0/[]$
• Rule: $f \circ id = f$
• Instantiation of the rule: $f$

So, the resulting tree will be:

$\xymatrix @!=.5pc { & = \ar@/^/[dl] \ar@/^/[dr]& \\f & & f \\}$

Resulting function: $f = f$.

From the rule of equality that we have $f = f$ is true and therefore it is true $f \circ swap \circ swap = f$

## Presentation

Time to show the software interface.

The program’s interface is divided into 3 parts:

### Input

Here the user can insert something that want to prove, for example:
$swap \circ swap = id$
$reverse \circ reverse = id$
$length \circ reverse = length$
and so on…

When you hit enter, you start having fun calculating :)

### Rules that may apply

Here you can navigate in the rules pressing PgUp or PgDn, and enter to aply the selected rule to the selected sub-expression.

### Proof state

Here you can browse the expression imagining it as the trees that showed earlier.

• up/down – to navigate into the levels
• left/right – no navigate into childs
• backspace – to make undo in the proof

We can also save and load proofs into XML, and also save proofs to PDF.

## Conclusion

Me and João still improving the pointfree calculator, and in the next year it will be used in one course here in Universidade do Minho.
The next stage we will implement type inference in the pointfree calculator, to make it powerfull. A lot of things have to be done, and in the next month we will start doing that, including make the first public release of the software.

If you understand Portuguese and want to see the presentation that we give in Department of Informatic in University of Minho:

### 5 responses

29 07 2008

Very nifty, will you make this software freely available ? I know that I myself wished for an UI quite like that (I imagined something more graphical, but your representation may be easier to work with in big trees).
It was in a wider context than pointfree computation though : I was using Coq and I noted that some very simple demonstrations became uselessly complex because of the lack of such a tool.

30 07 2008

[...] I said in previous post, one of the upgrades of Pointfree calculator is the type inference. After reading some scientific articles about Damas-Milner algorithm, also [...]

30 07 2008

Thank you for your comment. Not only do we distribute the Pointfree calculator free as we will also put it under an Open Source license. But that will only happen after program do type inference, because only then the calculator is indeed a powerful tool.
Today we already can do proofs for recursive functions, {cata, ana, hylo}morphisms, however it is still necessary to specify all of these morphisms rules for each data type. We want to be as general as possible. With the inference of types we will also increase the range of rules, because there are rules that work only on certain types of data.
Later I will announce when we start to distribute the software.

12 08 2008

Congrats mate! :) both of you have made a great job!
It is really inspiring observing you passion for FM.
I’m sure you’ll get far!

abraço! ;)

22 01 2009

This really is getting my brain working.