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.