non-recursive | Ulisses Costa Blog

Point-free over non-recursive functions II

12 03 2008

Off-topic

In the past two months I was in exams for my Lic. but now I have the time to continue with my post’s.

Back to my blog I find out that anyone can copy (CTRL+C) the images that are here and what in fact you are copying is the LaTeX code that I write to produce the images. That’s great! Now you can see my Xy-pic skills (lolz)…

Intro

In the last post of this series I have talk about Products of functions, in this post we will see more about point-free calculation using co-product of functions.

Because of the length of what I intend to explain I talk about these theme in three more post’s. Consider this part II.

Products (Part I)
Constants and conditionals (Part III)
Pointfree – Pointwise conversion & Program calculation (Part IV)

At the time I finish the other posts I will put their link here.

Part II

In this post I will talk about co-products of functions and some of their rules.

I will use $D_{\huge{E}}F$ that means ‘def’ from ‘definition’. I can’t use ‘def’ in this LaTeX package. And I confess that didn’t investigate a lot about that, in matter of fact I like the output of $D_{\huge{E}}F$ .

I will also use Commutative diagrams to explain the rules, Because I think that is the easy way to get it.

Combinators

I will use $\noindent (\odot)$ combinator defined in Part I.

either combinator

Like we sow for the structs (split combinator, Part I), we have also a combinator for unions (eithers).

The $(\nabla)$ is often called ’either’. This is the combinator responsible to take care of union’s (eithers in Haskell).

$\noindent \{D_{\huge{E}}F-\nabla\}:$
$(\nabla)~:~(a~\rightarrow~c)~\rightarrow~(b~\rightarrow~c)~\rightarrow~(a~+~b~\rightarrow~c)$
$(f~\nabla~g)~(Left~x)~=~f~x$
$(f~\nabla~g)~(Right~y)~=~g~y$

in Haskell became:

either :: (a -> c) -> (b -> c) -> Either a b -> c
either f g (Left x) = f x
either f g (Right y) = g y

As we will see with this combinator we can combine functions with the same counterdomain.

‘Left‘ and ‘Right‘ are constructors of data type Either (in Haskell) and we can see them as a functions with the folowing type:

$\noindent \{type-D_{\huge{E}}F-Left\}:$
$Left~:a~\rightarrow~a~+~b$

$\noindent \{type-D_{\huge{E}}F-Right\}:$
$Right~:b~\rightarrow~a~+~b$

As you can see with both functions we can inject information in our functions, in the oposite side we have ´fst´ and ´snd´ functions that we use to project information (Part I).

Let A, B, C, D be Types and f : A -> C, g : B -> C and we want the function either : A + B -> C

Like diagram is commutative we can infer two rules:

$\noindent \{univ-+\}:$
$either = f \nabla g \Leftrightarrow either \odot Left = f \wedge either \odot Right = g$

$\noindent \{cancel-+\}:$
$(f \nabla g) \odot Left = f$
$(f \nabla g) \odot Right = g$

Now, if type C = A + B, we will have $f \nabla g : A + B \rightarrow A + B$

To have a commutative diagram we must have $f = Left$ and $g = Right$

And we can infer the rule:

$\noindent \{reflex-+\}:$
$Left \nabla Right = id_{A + B}$

Let A, B, C, D be Types and g : A -> C, h : B -> C and f : C -> D.

$\noindent \{fusion-+\}:$
$f \odot (g \nabla h) = f \odot g \nabla f \odot h$

$\bigoplus$ combinator

When we want to defin a function that takes a co-product and goes to a co-product we may use the function (\bigoplus)

$\noindent \{D_{\huge{E}}F-\bigoplus\}:$
$\noindent f \bigoplus g~=~Left \odot f \nabla Right \odot g$

in Haskell became:

infixr 4 -|-

(-|-) :: (a -> b) -> (c -> d) -> Either a c -> Either b d
f -|- g = either (Left . f) (Right . g)

here is the diagram of it definition:

$\noindent \{abssoc-+\}:$
$(f \nabla g) \odot (h \bigoplus i) = f \odot h \nabla g \odot i$

$\noindent \{functor-+\}:$
$(f \bigoplus g) \odot (h \bigoplus i) = f \odot h \bigoplus g \odot i$

We also have the equalty of eithers;

$\noindent \{eq-\bigoplus\}:$
$(f \nabla g) = (h \nabla k) \Leftrightarrow f = h \wedge g = k$

And, to conclude, we have a rule that relationate ‘eithers’ with ‘splits’,

$\noindent \{change-law\}:$
$(f \Delta g) \nabla (h \Delta k) = (f \nabla h) \Delta (g \nabla k)$

examples

To show you some of the power of program calculation here is the prove of $\noindent \{change-law\}:$

(please open the image to see it in full size)

$\noindent(f \Delta g) \nabla (h \Delta k) = (f \nabla h) \Delta (g \nabla k)\\\Leftrightarrow \{nat-id, reflex-\bigoplus\}\\(f \Delta g) \nabla (h \Delta k) = (f \nabla h)\Delta (g \nabla k) \odot (Left \nabla Right)\\\Leftrightarrow \{fusion-\bigoplus\}\\(f \Delta g) \nabla (h \Delta k) = ((f \nabla h) \Delta (g \nabla k)) \odot Left \nabla ((f \nabla h) \Delta (g \nabla k)) \odot Right\\\Leftrightarrow \{eq-\bigoplus\}\\f \Delta g = (f \nabla h) \Delta (g \nabla k) \odot Left\\\wedge\\h \Delta k = (f \nabla h) \Delta (g \nabla k) \odot Right\\\Leftrightarrow \{fusion-\bigotimes\}\\f \Delta g = ((f \nabla h) \odot Left ) \Delta ((g \nabla k) \odot Left)\\\wedge\\h \Delta k = ((f \nabla h) \odot Right) \Delta ((g \nabla k) \odot Right)\\\Leftrightarrow \{cancel-\bigoplus\}\\f \Delta g = f \Delta g\\\wedge\\h \Delta k = h \Delta k\\\Leftrightarrow {TRUE}\\TRUE$

Notes

The $\odot$ combinator have more precedence than the $\nabla$ combinator.
So, $((f \Delta h) \nabla (g \Delta k)) \odot Left = (f \Delta h) \nabla (g \Delta k) \odot Left$

Aknowledgements

I would like to thank dysfunctor to the corrections made to this post.

Comments : 4 Comments »
Tags: English, haskell, mathematics, non-recursive, pointfree, software
Categories : Uncategorized

Point-free over non-recursive functions I

10 01 2008

Intro

Like I promise I will talk about point-free over non recursive functions.
Point-free style is used to demonstrate propriety over programs easily than pointwise.
Because we didn’t have variables in functions, we can compose a lot of small functions with each other using some combinators.
Those combinators have some rules associate with them that tell us when to use some combinator.Also because I think that’s the easy way to learn point-free programming style. I will talk about that style over non recursive functions.

Because of the length of what I intend to explain I will talk about these theme in three more post’s. Consider this part I.

In the following parts I will talk about:

Co-Products (Part II)
Constants and conditionals (Part III)
Pointfree – Pointwise conversion & Program calculation (Part IV)

At the time I finish the other posts I will put their link here.

Part I

In this post I will talk about products of functions and some of their rules.

I will also use Commutative diagrams to explain the rules, Because I think that is the easy way to get it.

Combinators

The combinator $\noindent (\odot)$ is the fundamental for point-free style.

$\noindent \{D_{\huge{E}}F-\odot\}:$
$\noindent (\odot)~:~(b~\rightarrow~c)~\rightarrow~(a~\rightarrow~b)~\rightarrow~(a~\rightarrow~c)$
$(f~\odot~g)~x~=~f~(g~x)$

In fact $\noindent (\odot)$ is the fundamental combinator in Mathematical analysis.

Another very important function is the $\noindent id$ function, the identity.

$\noindent \{D_{\huge{E}}F-id\}:$
$\noindent id~:a~\rightarrow~a$
$id~x~=~x$

$\noindent (\odot)$ and $\noindent id$ respect the following laws:

$\noindent \{assoc-\odot\}:$
$\noindent (f \odot g) \odot h~=~f \odot (g \odot h)$

$\noindent \{nat-id\}:$
$\noindent f \odot id~=~f~=~id \odot f$

With just those laws we are ready to demonstrate programs, like:

Let A, B, C, D be Types and f :: A -> B, g :: B -> C and h :: C -> D

let’s prove that
$\noindent (h \odot g) \odot (id \odot (f \odot id)) = h \odot (g \odot f)$

To demonstrate this equality we pick one of the sides of the equation, and with $\noindent \{nat-id\}$ and $\noindent \{assoc-\odot\}$ , we try to obtain the other side.

In this case, we can do:

$\noindent (h \odot g) \odot (id \odot (f \odot id)) = h \odot (g \odot f)$
$\Leftrightarrow \{assoc-\odot\}$
$((h \odot g) \odot id) \odot (f \odot id) = h \odot (g \odot f)$
$\Leftrightarrow \{nat-id\}$
$(h \odot g) \odot (f \odot id) = h \odot (g \odot f)$
$\Leftrightarrow \{assoc-\odot\}$
$((h \odot g) \odot f) \odot id = h \odot (g \odot f)$
$\Leftrightarrow \{nat-id\}$
$(h \odot g) \odot f = h \odot (g \odot f)$
$\Leftrightarrow \{assoc-\odot\}$
$h \odot (g \odot f) = h \odot (g \odot f)$
$\Leftrightarrow TRUE$

1) In fact as a convenience we can take off the brakets in a sequence os compositions. And so is pointless the use of $\noindent \{assoc-\odot\}$ law.
2) We can also use more than one rule per line.

So, the previous demonstation becames:

$\noindent (h \odot g) \odot (id \odot (f \odot id)) = h \odot (g \odot f)$
$\Leftrightarrow \{1,1\}$
$h \odot g \odot id \odot f \odot id = h \odot g \odot f$
$\Leftrightarrow \{nat-id,nat-id\}$
$h \odot g \odot f = h \odot g \odot f$
$\Leftrightarrow TRUE$

split combinator

In any programming language we always have two general types to aggregate data, struct’s and unions.
Now we will see two combinators that work with those data types.

The $(\Delta)$ is often called ‘split’. This is the combinator responsible to take care of struct’s (tuples in Haskell).

It definition is:

$\noindent \{D_{\huge{E}}F-\Delta\}:$
$(\Delta)~:~(c~\rightarrow~a)~\rightarrow~(c~\rightarrow~b)~\rightarrow~(c~\rightarrow~a \times b)$
$(f~\Delta~g)~x~=~(f~x,g~x)$

in Haskell became:

split :: (c -> a) -> (c -> b) -> c -> (a,b)

split f g x = (f x, g x)

This combinator allow, as well, combine functions with the same domain.

With the functions ‘fst’ and ‘snd’ we can access the content of a tuple.

fst (a,b) = a

snd (a,b) = b

Let A, B, C, D be Types and f : A -> B, g : A -> C and we want the function split : A -> B x C

Like diagram is commutative we can infer two rules:

$\noindent \{univ-\times\}:$
$split = f \Delta g \Leftrightarrow fst \odot split = f \wedge snd \odot split = g$

$\noindent \{cancel-\times\}:$
$fst \odot (f \Delta g) = f$
$snd \odot (f \Delta g) = g$

Now, if type A = B x C, we will have $f \Delta g : B \times C \rightarrow B \times C$

To have a commutative diagram $f = fst$ and $g = snd$

And we can infer the rule:
$\noindent \{reflex-\times\}:$
$fst \Delta snd = id_{B\times C}$

Let A, B, C, E be Types and h : A -> B, f : B -> C and g : B -> E.

$\noindent \{fusion-\times\}:$
$(f \Delta g) \odot h = f \odot h \Delta g \odot h$

Example – isomorphism demonstration

As example we can demonstrate isomorphisms.
Here is a brief description:

To prove the isomorphism $a \cong b$ we have to find two functions:
$f : a \rightarrow b$ and $g : b \rightarrow a$ such that $f \odot g = id \wedge g \odot f = id$

To do that we can use the diagrams or doscover the pointwise version and them converte to point-free, I will show later on the last techique.

Now we gonna use the diagrams to show the isomorphism $a \times (b \times c) \cong c \times (b \times a)$ .

Discovering g:

So, the definition of the function h is:
$h : a \times(b \times c) \rightarrow c \times (b \times a)$
$h = snd \odot snd \Delta (fst \odot snd \Delta fst)$

Discovering $g^{\bullet}$

So, the definition of the function $h^{\bullet}$ is:
$h^{\bullet} : c \times (b \times a) \rightarrow a \times(b \times c)$
$h^{\bullet} = snd \odot snd \Delta (fst \odot snd \Delta fst)$

And we conclude $h \odot h^{\bullet} = id = h^{\bullet} \odot h$ , so we prove $a \times (b \times c) \cong c \times (b \times a)$

$\bigotimes$ combinator

When we want to defin a function that takes a product and goes to a product we may use the function $(\bigotimes)$

$\noindent \{D_{\huge{E}}F-\bigotimes\}:$
$\noindent f \bigotimes g~=~f \odot fst \Delta g \odot snd$

in Haskell became:

infixr 5 > b) -> (c -> d) -> (a, c) -> (b, d)

(f >< g) x = split (f . fst) (g . snd)

here is the diagram of it definition:

The folowing diagram,

coud be simplified into this one:

And so, we find another rule:

$\noindent \{abssoc-\times\}:$
$(f \bigotimes g) \odot (h \Delta i) = f \odot h \Delta g \odot i$