31 07 2008

Intro

When I was studding yacc noticed that there was much information available, not something one would expect of a tool with 40 years. Unfortunately there was no quick learning for someone who already knew the whole theory behind this kind of tools. As I said, the yacc is a very old tool, made when was needed compilers. Before there the whole theory of that area that we know today. So it is normal small errors transform themselves into disasters that may take a long time to be resolved.

This post is for those who already know what grammars are, lexical analyzers, etc., but that never touch in Lex/yacc or for those who are stuck with this things (I hope).

In this post I will explain to you Lex/yacc, with an example of a program that I did. I will not boring you with massive lines of code (like I usually do), because Lex/yacc is just a simple tool to use. With just 60 lines of explained code you will see how great that is.

The problem

My idea was to do a simple site with all the information about all the cities in Portugal. After reminded me to so but to all parishes (Freguesia in Portuguese), counties(Concelho in Portuguese) and districts(Distrito in Portuguese) of Portugal and their relationship. A district has many counties and one county has many parishes.

Simple! What I needed now was all the names of all parishes, counties and districts of Portugal, I eventually found three files with all this information and more in the Portuguese company of post office website. Better yet, these files had the relationship between each division. I have to do a small program in C that take those three files and create a new file, which I use on the Lex / yacc.

In order to have all available information on each local od Portugal I decided to use Wikipedia. This is the Achilles heel of the program, because unfortunately the entries of wikipedia on the Portuguese parishes are not uniform and many of the parishes or have entry. But still able to have good results.

The structure of the new file generated is:

District1>WikipediaEntry_for_District1
Parish1_of_Countie1>WikipediaEntry_for_Parish1_of_Countie1,
Parish2_of_Countie1>WikipediaEntry_for_Parish2_of_Countie1,
Parish3_of_Countie1>WikipediaEntry_for_Parish3_of_Countie1,
.
.
.
ParishN_of_Countie1>WikipediaEntry_for_ParishN_of_Countie1
!Countie1>WikipediaEntry_for_Countie1;
Parish1_of_Countie2>WikipediaEntry_for_Parish1_of_Countie2,
Parish2_of_Countie2>WikipediaEntry_for_Parish2_of_Countie2,
Parish3_of_Countie2>WikipediaEntry_for_Parish3_of_Countie2,
.
.
.
ParishN_of_Countie1>WikipediaEntry_for_ParishN_of_Countie2
!Countie2>WikipediaEntry_for_Countie2;
.
.
.
!CountieN>WikipediaEntry_for_CountieN|

District2>WikipediaEntry_for_District2
Parish1_of_Countie1>WikipediaEntry_for_Parish1_of_Countie1,
Parish2_of_Countie1>WikipediaEntry_for_Parish2_of_Countie1,
Parish3_of_Countie1>WikipediaEntry_for_Parish3_of_Countie1,
.
.
.
ParishN_of_Countie1>WikipediaEntry_for_ParishN_of_Countie1
!Countie1>WikipediaEntry_for_Countie1;
Parish1_of_Countie2>WikipediaEntry_for_Parish1_of_Countie2,
Parish2_of_Countie2>WikipediaEntry_for_Parish2_of_Countie2,
Parish3_of_Countie2>WikipediaEntry_for_Parish3_of_Countie2,
.
.
.
ParishN_of_Countie1>WikipediaEntry_for_ParishN_of_Countie2
!Countie2>WikipediaEntry_for_Countie2;
.
.
.
!CountieN>WikipediaEntry_for_CountieN|
.
.
.

It have about 43000 lines, the number of parishes in Portugal.

Yacc

An Yacc file is just like an lex file, it is divided in three parts:

DECLARATIONS
%%
GRAMMAR
%%
FUNCTIONS

I Will explain later on, what to put in all those three parts.

The solution

I start to write the following grammar to describe my new file:

OrGeo     -> Districts

Districts -> District '|'
| Districts District '|'

Counties -> Countie
| Counties ';' Countie

Countie  -> Parishes '!' IdC Link

Parishes    -> Parish
| Parishes ',' Parish

IdD       -> id

IdC       -> id

IdL       -> id

As id is a name (of the District, Countie or Parish), we will declare it in yacc as a pointer to chars (vals). To do that we create a union like in the first part of yacc file (DECLARATIONS), and add a association with vals with id and l:

%union {
char *vals;
}

%token  id l

Yacc use that union because you can declare as many associations as you want. We must refer to that union in the lex as yylval.

This is the same as use:

%token  id
%token  l

We now go to lex file and add the rule that the lexical analyzer will meet when find text.

[ a-zA-ZÀ-ú-'.()/'0-9]+  { yylval.vals = strdup(yytext);
return id; }
[a-zA-ZÀ-ú-'.()/'0-9_:]+ { yylval.vals = strdup(yytext);
return l; }

Here we are saying that when lex find some text that fills in that regular expression it will return to yacc as an id, so that way we find the names of our cities, or links.

As you can see we have special symbols in our grammar, (!>,;|), so we need to say to lex to return them to yacc, where we need them:

[!>,;|]                           { return yytext[0]; }

I also will say to lex ignore all n and t characters:

[tn]                            { ; }

Making our grammar powerfull

Now our grammar will suffer some adjustments; we will say yacc what to do when it was in some of the derivations of some rule:

OrGeo     : Districts { d = $1; } ; Districts : District '|' { $$= 1; } | Districts District '|' {$$ = catDistricts($1,$2); } ; District : IdD Link Counties { $$= addDistrict(1, 2, 3); } ; Counties : Countie {$$ =$1; }
| Counties ';' Countie { $$= catCounties(1, 3); } ; Countie : Parishes '!' IdC Link {$$ = addCountie($1,$3, $4); } ; Parishes : Parish { $$= 1; } | Parishes ',' Parish {$$ = catParishes($1, $3); } ; Link : '>' l { $$= 2; } ; IdD : id {$$ =$1; }
;
IdC       : id { $$= 1; } ; Parish : IdL Link {$$ = addParish($1,$2); }
;
IdL       : id { $$= 1; } ; Here we tell yacc how to behave when pass certain derivation of a rule. We can tell yacc that some rule can return a data type, for example: %{ #include #include #include "district.h" District *d; %} %union { char *vals; Parish *valf; Countie *valc; District *vald; } %type Link IdL IdD IdC %type Parish Parishes %type Countie Counties %type District Districts To return something in a rule we refer to that rule as$$, that mean IdL in

IdL       : id

and $1 to refer to that id, and so on. So, that way we can say that$$=$1, that means, IdL = id.

The result is a html page with nested liked lists, here is the result.

Notes

All the code, including the code to generate the new file, used to yacc is available here, fell free to use it.

30 07 2008

Intro

The type inference is the ability to a programming language deduct the data types of all functions of a program. It is a feature present in many strongly typed languages, such as Haskell. Where is not mandatory write the signature of the functions. What is great because it increases the production of code, and security because if the inference algorithm fail means that we have an error of types in our code, all this in compilation time.

As 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 known as W algorithm, I began to imagine a way to implement this in Java, which is the mother language of Pointfree calculator. I started to do some sketches on paper and, after talking with professor José Nuno Oliveira, I realize that the algorithm isn’t that hard.

Remainings

Definition of $(\nabla)$ (either in Haskell):

NOTE: $+$ in types means Either in Haskell

$(\nabla)~:~(a~\rightarrow~c)~\rightarrow~(b~\rightarrow~c)~\rightarrow~a+b~\rightarrow~c$
$(\nabla)~f~g~(Left~a)~=~f~a$
$(\nabla)~f~g~(Right~b)~=~g~b$

Definition of $(+)$:
$(+)~:~(a~\rightarrow~b)~\rightarrow~(c~\rightarrow~d)~\rightarrow~a+c~\rightarrow~b+d$
$f + g = (Left \circ f)\nabla(Right \circ g)$

Type signature of Left and Right:

$Left~:~a\rightarrow~a+b$
$Right~:~b\rightarrow~a+b$

Talking same language

I will use a different notation to represent the domain and codomain of functions in order to help the explanation of the algorithm.

For $(+)$ function we have the type:

$(+)~:~(a~\rightarrow~b)~\rightarrow~(c~\rightarrow~d)~\rightarrow~a+c~\rightarrow~b+d$

I will write that as:

$(f_{a}^{b} + g_{c}^{d})_{a+c}^{b+d}$

Remember the definition of $(+)$, we receive two functions, f and g. Because the notation is in pointfree, we represent also de domain and codomain of function $(f + g)$ in front of that, like we do for f and g.
In fact the type of $(f + g)$ is represented as:

$(f + g)~:~a+c~\rightarrow~b+d$

I will also use the symbol $a \sim b$, to say that type a unify with type b, that means, informally, that $a = b$.

Let’s infer!

I will explain the algorithm to infer the type of function f:

$f = (id + Left) \nabla (Right \circ Right)$

The first step of the algorithm is attribute to all functions polymorphic types, so I will call the first type $t_1$ and the last $t_n$ $\forall_{1,\ldots,n}\in\mathbb{N}$

$\begin{array}{|l|}\hline((id_{{\color{blue}t_1}}^{{\color{blue}t_2}} + Left_{{\color{blue}t_3}}^{{\color{blue}t_4}})_{{\color{blue}t_5}}^{{\color{blue}t_6}} \nabla (Right_{{\color{blue}t_7}}^{{\color{blue}t_8}} \circ Right_{{\color{blue}t_9}}^{{\color{blue}t_{10}}})_{{\color{blue}t_{11}}}^{{\color{blue}t_{12}}})_{{\color{blue}t_{13}}}^{{\color{blue}t_{14}}}\\\hline\end{array}$

Because, $id$ have type $id~:~a\rightarrow~a$, we conclude $t_2 \sim t_1$;
Also, because $Left$ have the type $Left~:~a\rightarrow~a+b$, we can conclude $t_4 \sim t_3 + t_4$;
Same thing to $Right$, that have the type $Right~:~b\rightarrow~a+b$, we can conclude $t_8 \sim t_8 + t_7$ and $t_{10} \sim t_{10} + t_9$, so we have:

$\begin{array}{|l|}\hline\Leftrightarrow \{t_2 \sim t_1, t_4 \sim t_3 + t_4, t_8 \sim t_8 + t_7, t_{10} \sim t_{10} + t_9 \}\\\hline\end{array}$

$\begin{array}{|l|}\hline((id_{t_1}^{{\color{blue}t_1}} + Left_{t_3}^{{\color{red}t_3+t_4}})_{t_5}^{t_6} \nabla (Right_{t_7}^{{\color{green}t_8+t_7}} \circ Right_{t_9}^{{\color{green}t_{10}+t_9}})_{t_{11}}^{t_{12}})_{t_{13}}^{t_{14}}\\\hline\end{array}$

Because, the definition of $\circ$: $f \circ g = f(g(x))$, we can say that the domain of f is equal to codomain of g, and so we can conclude $t_7 \sim t_{10}+t_9$, as we replace a type that is used in the codomain of first Right, we must also conclude $t_8 + t_7 \sim t_8 + (t_{10} + t_9)$, so:

$\begin{array}{|l|}\hline\Leftrightarrow \{t_7 \sim t_{10}+t_9 \Rightarrow t_8 + t_7 \sim t_8 + (t_{10} + t_9) \}\\\hline\end{array}$

$\begin{array}{|l|}\hline((id_{t_1}^{t_1} + Left_{t_3}^{t_3+t_4})_{t_5}^{t_6} \nabla (Right_{{\color{blue}t_{10}+t_9}}^{{\color{red}t_8+(t_{10}+t_9)}} \circ Right_{t_9}^{{\color{blue}t_{10}+t_9}})_{t_{11}}^{t_{12}})_{t_{13}}^{t_{14}}\\\hline\end{array}$

As I explain before, the function $(+)$, have the following type: $(f_{a}^{b} + g_{c}^{d})_{a+c}^{b+d}$, so:
$t_6 \sim t_1+(t_3+t_4)$ and $t_5 \sim t_1+t_3$;
Because $f \circ g$ have the type: $(f_{a}^{b} \circ g_{c}^{d})_{c}^{b}$, so $t_{12} \sim t_8+(t_{10}+t_9)$ and $t_{11} \sim t_9$:

$\begin{array}{|l|}\hline\Leftrightarrow \{t_6 \sim t_1+(t_3+t_4), t_5 \sim t_1+t_3 ,\\ t_{12} \sim t_8+(t_{10}+t_9), t_{11} \sim t_9\}\\\hline\end{array}$

$\begin{array}{|l|}\hline((id_{t_1}^{t_1} + Left_{t_3}^{t_3+t_4})_{{\color{blue}t_1+t_3}}^{{\color{blue}t_1+(t_3+t_4)}} \nabla\\ (Right_{t_{10}+t_9}^{t_8+(t_{10}+t_9)} \circ Right_{t_9}^{t_{10}+t_9})_{{\color{red}t_9}}^{{\color{red}t_8+(t_{10}+t_9)}})_{t_{13}}^{t_{14}}\\\hline\end{array}$

Because the definition of $(\nabla)$ is $(f_{a}^{b} \nabla g_{c}^{b})_{a+c}^{b}$, we need the same codomain in both functions, so we conclude $t_1+(t_3+t_4) \sim t_8+(t_{10}+t_9)$, as both type trees have the same structure, we can conclude even more: $t_1 \sim t_8 \wedge t_3 \sim t_{10} \wedge t_4 \sim t_9$, so:

$\begin{array}{|l|}\hline\Leftrightarrow \{t_1+(t_3+t_4) \sim t_8+(t_{10}+t_9) \Rightarrow\\ t_1 \sim t_8 \wedge t_3 \sim t_{10} \wedge t_4 \sim t_9\}\\\hline\end{array}$

$\begin{array}{|l|}\hline((id_{t_1}^{t_1} + Left_{t_3}^{t_3+t_4})_{t_1+t_3}^{t_1+(t_3+t_4)} \nabla\\ (Right_{{\color{blue}t_3}+{\color{green}t_4}}^{{\color{red}t_1}+({\color{blue}t_3}+{\color{green}t_4})} \circ Right_{{\color{green}t_4}}^{{\color{blue}t_3}+{\color{green}t_4}})_{{\color{green}t_4}}^{{\color{red}t_1}+({\color{blue}t_3}+{\color{green}t_4})})_{t_{13}}^{t_{14}}\\\hline\end{array}$

And now we have the function, just with the needed types to simplify:

$f_{t_{13}}^{t_{14}} = (id + Left)_{t_1+t_3}^{t_1+(t_3+t_4)} \nabla (Right \circ Right)_{t_4}^{t_1+(t_3+t_4)}$.

Now we just need to unify: $t_{14} \sim t_1+(t_3+t_4)$ and $t_{13} \sim (t_1+t_{3})+t_4$,

$\begin{array}{|l|}\hline\Leftrightarrow \{t_{14} \sim t_1+(t_3+t_4), t_{13} \sim (t_1+t_{3})+t_4\}\\\hline\end{array}$

$f_{{\color{red}(t_1+t_{3})+t_4}}^{{\color{blue}t_1+(t_3+t_4)}} = (id + Left)_{t_1+t_3}^{t_1+(t_3+t_4)} \nabla (Right \circ Right)_{t_4}^{t_1+(t_3+t_4)}$.

We infer the type for function $f = (id + Left) \nabla (Right \circ Right)$, $f : (t_1+t_3)+t_4 \rightarrow t_1+(t_3+t_4)$.
Or if you prefer; in Haskell:

f :: Either (Either a b) c -> Either a (Either b c)

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: