the category of Relations is a 2-category

The category of relations with:

• 0-cells : Sets (A,B,C,D)
• 1-cells : Relations(R,S, T)
• 2-cells : Inclusion. R < S iff forall x:A, y:B, xRy implies xSy

1. Horizontal composition: R < R' S < S' implies R.S < R'.S'
2. Vertical composition : R < S < T imples R < T

Am I right?

notes on Ur/Web's fold function

This post is about Ur/Web Programming language at
http://www.impredicative.com/ur
it's a detail document on fold function, a type level folding function.

	Description	Example
val fold : K	a kind, one of Type, Name, or Unit.	Type
--> tf :: ({K} -> Type)	a type level function, given a record of K, return a Type,	con numFields = fn _ => int
	Following is a type level folder function.
	Given a value of type tf r, return a value of type tf ([ nm=v] ++r )
-> (nm :: Name ->	nm is a name,	Male
v :: K ->	v is a type of kind K,	bool
r :: {K} ->	rest of the record.	[ Name = string , Age = int]
[[nm] ~ r]	a prove of nm is not in r. The compiler will prove for you.	Prove of Male is not in { Name, Age}
=>	all arguments before => are type level, and can be deduced by compiler.
tf r ->	given a value of type tf r.	5
tf ([nm = v] ++ r))	return a value of type tf( [nm=v]++r)).	6
-> tf []	initial value, it has type tf [], [] is the empty record ( type level )	0
-> r ::: {K}	record to fold.	{ Name : "Alex", Age : 10 , Male : False}
-> folder r	a folder that will derived by the compiler
-> tf r	return type. eg. int	3

A symmetric list type

In almost all functional programming language ( ML, Haskell) , list is defined as below ( in Isabelle syntax )

datatype 'a list =
Nil
| Cons 'a "'a list" (infixl "#" 65)

The symmetry of list is lost in above definition ,
which also cause the proof of list property extremely hard

If you look at the page 10 to 15 of
http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2011/doc/tutorial.pdf
you'll find the prove rev (rev x) = x is quite long ,
with the introduction of 5 lemma.
but if we defined list symmetrically , we don't need to define append function , and prove of rev(rev x ) = x is just a piece of cake.
following is the Isabelle code:

theory List1
imports Datatype
begin


datatype 'a list =
S 'a
| Cons "'a list" "'a list" (infixl "#" 65)

primrec rev :: "'a list \ 'a list" where
"rev (S x ) = S x "
| "rev (x # y) = rev y # rev x "


theorem rev_rev [simp] : "rev (rev x ) = x "
apply (induct_tac x)
apply(auto)
done


Problem :
I cannot prove associative of # .
This makes me understand why lists are defined as cons a (list a) ,
because cons a ( cons b (cons c nil)) is the normal form.
and you can prove associative from the normal form.
while my way of defining list do not have normal form.

notes on relation algebra

From : Graham , Between Functions and Relations in Calculating Programs

Calculational approach to programming ( derive program from specification):

• fold/unfold of Burstall and Darlingto
• imperative refinement calculus of Back Morgan , Morris 
• functional Squiggol of Bird and Meertens
• relational Ruby of Jones and Sheeran
• categorical approach of Bird and De Moor   
• From Dynamic Programming to greedy algorithm
• Oege . Categories, Relations and Dynamic Programming

History of Binary Relation Theory:

• Peirce 1870
• Schroder 1895
• Tarski 1941 .On the calculus of relations 

Relational calulus as Programming Language

• Ruby , Jones and Sheeran
• Bird and de Moor 
• Backhouse el.  A relational theory of datatypes
• MacLennan RPL 
• D. M. Cattrall . The Design and Implementation of a Relational Programming System. Phd
• Veloso. Partial relations for program derivation.

Developement of Squiggol

• Boom Hierarchy: tree , lists, bags, sets
• Malcom : recursive types , F-algebra, catamorphic. Algebraic Data Types and Program Transformation. PhD.
• Gibbons 29
• Meijer 50. types are cpo. unify finite and infinite objects , deriving compiler from denotational semantics. 
• Fokkinga 27. extend F-algebra to constructors with laws. Law and Order in Algorithmics. PhD.
  

Relational Algebra as specification 

• Berghammer [7]. specify types and programs
• Desharnais [21]. specify types by relational formulae
• Haeberer [67]. extend RA to first order logic
• Fredy [28]. Barr[6], Carboni [16]Categorical treatment

Unfinished. 

Picture Proves

Do you ever walk through a proof, understand each step, yet not believe the 

theorem, not say ‘Yes, of course it’s true’? The analytic, logical, sequential 

approach often does not convince one as well as does a carefully crafted 

picture. This difference is no coincidence. The analytic, sequential portions 

of our brain evolved with our capacity for language, which is perhaps 105 

years old. Our pictorial, Gestalt hardware results from millions of years 

of evolution of the visual system and cortex. In comparison to our visual 

hardware, our symbolic, sequential hardware is an ill-developed latecomer. 

Advertisers know that words alone do not convince you to waste money on 

their clients’ junk, so they spend zillions on images. This principle, which has 

higher applications, is the theme of this chapter. 

http://ocw.mit.edu/NR/rdonlyres/Mathematics/18-098January--IAP--2008/FFEA8D92-1210-46A9-8D43-931D4A43D87C/0/sf_math.pdf

quote from Street Fighting Mathematics.

From concrete to abstract

    Most of introduction on Category theory starts with the definition of a category first,
then give some example. Which I believe is wrong.
    It's same wrong way that we are taught on mathematics in university.

Teaching definition, theory first, then give example, exercise is a totally wrong way of teaching math.
This way assume gives us a few axioms, rules, then we can reduce the whole mathematic world,
we can select rule and axioms to solve problem, which is totally wrong.
This way assume human as a computer, a rule deduction system, but think this way:
    assuming we have 1 axiom
    by simple replace rule, we get 1 corollaries.
    so next step , we have to choose from 2 (axiom + corollaries)
    and next , we apply replace rule, get 1 more corollaries, now we have 3 choices. ...
    the search space is 1 * 2 * 3 * 4 ..   = n!
obviously , human mind are not good at this way of thinking. Just take a look how popular of simple
puzzle games on iTune, you can agree with me.

From my own personal experience,  my brain never works this way. It can easily image a 2d image,
then remember there a 7 corollaries.

I believe Feynman( a great physicist) learning mathematics by himself. From a book I ready about him,
he seemed invented a whole system about mathematics by him own, and one day , when he discuss with
other classmate, he found nobody can understand him.

So my point is : mathematics should be learned by yourself, not taught by someone.
Give yourself a few problems, maybe not math problem, solve them, find the common things between them, abstract them .
Example 1 :  we found
    (1 + 2 ) * 3 = 9 = 1*3 + 2 * 3
    (2 + 3) * 4 = 4 * 2 + 4 * 3
    ...
so what's common among them ? think yourself before reading.
( This is important , and maybe the only way to learn math . Think yourself before reading )
 What's common : two numbers add first , then multiply a third number, can multiply to the third number each first, then add.
But the above sentence is too verbose, the third number appeared twice, how about we replace it with z?
also, what number here is not important, how about we use x, y to represent any number?
so we get

          (x +y) * z = x *z + y *z                            (1)

Now we get Algebra : using x,y,z to represent any numbers, we found equations that can be used to any numbers!!

This might seemed to be to simple for most of adults, some let continue to some difficulty ones.

we already might now
     x ^ (m+n) = x^m * x^n                       (2)

( ^ is for power , 2 ^3 = 8, 2 ^ 4 = 16)
so what's common about (1) and (2) ??? ( Think, before you continue)

first , I'll change some variable in (2) to get some hint.
      z ^ ( x + y) = z ^ x * z ^ y                  (3)
      z * ( x + y) = z * x + z * y                  (4)
secondly, there are too many z^ in (3), how about we use f to replace z^ ?
     f(x+y) = f x * f y                                  (5)
use g to replace z*
     g(x+y) = gx + gy                                  (6)

so now we have the concept of function !

But still, the x,y in (5) and (6) appeared twice, can we remove it ?  (Think !!)
how about we image + (add symbol ) as a pipe with 2 input, 1 output ?
and f as a pipe of 1 input , 1 output ? so f(x+y) become
x --->
           +    ---> f  --->  f(x+y)
x --->

for simplicity , we just write
     + f
to represent above picture.
Now your exercise : draw picture of fx * fy
     f(x+y) = fx * fy will change to

-->               --> f
       +  f  =              *
-->               --> f

we use II f to represent a pair of f , so
  + f = (II f)   *             (7)

now can you image we can use (7) to represent both z* (x+y) = z *x + z*y and z^(x+y) = ...?

Now take a look at the pair  II , it take a function ( pipe), and return a pair of pipe ! It's a functor  !
Also we found a lot of binary function  has equations like (7), so we abstract the concept of binary operator , and get
   b1 f = (II f) b2    where b1 ,b2 are binary function.  (8)

I'm a little lazy now, but I'm telling you (8) can be abstract again to get homomorphism, 
and natural  transformation , category .....

The following link is a good article worth reading .
http://betterexplained.com/articles/developing-your-intuition-for-math/

Readability of programming

The readability of a piece of code depends on following staff:

• Background knowledge
• Input of a function
• Output
• intermedia  result

To improve readability, there should be a way to visualize how the data are processed by each line of code.