August 05, 2007

DFAs, Categories, and Typecheckers.

I've recently started reading (in parallel) "Type and Programming Languages" and "Basic Category for Computer Scientists." The latter of which is really only interesting if you're a math junky, like me. It's somewhat dry, and very matter-of-fact, but the subject is terribly interesting.

Whilst reading these books, I've also been working on a library for Haskell called "HFA" (pronounced: "Huffa", or if your feeling silly, "Hoffa"), for "Haskell Finite Automata." The library's purpose is to create a simple to use, generic, relatively fast implementation of various Automata (Notably (D|N)FA's, PDAs, Turing Machines, etc.), so that anyone intending to use these abstractions will be able to without knowing much about the internal theory, eg how to minimize a DFA, or how to convert an NFA to a DFA, etc. It's also intended to be available as a easy to understand tool for learning/teaching about automata, it will eventually have the ability to display Automata as Graphviz graphs, and is currently capable of generating state diagrams (with some extensions to mark final, initial, and initial-final states).

Recently, I had just finished writing some refactor code for HFA, and decided to take a break and read "Basic Category Theory" for a while, it dawned on me upon looking at the diagram of a category that what I was looking at was essentially a DFA, with all states final, and the arrows between them being processing parts of the Delta Functions. That is, if a Category is defined as a a set of objects, and a set of arrows (where an arrow is defined as f : A -> B, where A and B are objects in the category), then the equivalency is as follows:


Category DFA
Objects States
Arrows Transitions

with delta(S,x) = S' iff there is an arrow between x is an arrow between S and S'.

Notably, we can also define a DFA as a Category by simply reversing the definition. I'm pretty sure this fact has been discovered before, its to obvious to believe otherwise (though it would be cool I could name this "The Fredette Isomorphism", ^_^). The interesting thing about this Isomorphism is that, if we can generalize a DFA, whats to say that we couldn't generalize the category in the same way? Take Imperative languages for instance. I don't know if it works out (and I certainly don't have the skill to prove it if it does work out, at least not yet), but it is a hypuothesis of mine that an imperative program can be represented in a category with multiple arrows going from one object to another simultaneously, that is, an imperative program is a kind of "Nondeterministic" category. Ring any bells? We know (by the simple fact of Turing completeness) that a TC imperative language program can be written in a TC Pure Functional language (assuming there's a Pure Functional way to deal with State, eg Monads). Similarly (and this is almost to much of a guess to even _think_ of it as a hypothesis) if a TC Imperative Language is a "Nondeterministic" (ND) category, then if a ND Category is isomorphic to a NFA, then we know that NFA's are isomorphic to DFA's, and we know that Pure Functional Languages are isomorphic to operations withing a "Deterministic" Category, eg a "DFA", so that would "prove" (I use that term _very_ loosely) that any old TC Imperative program has an equivalent TC Pure Functional Program.

Pretty Neat, huh? It probably doesn't work somewhere, but still- it's cool.

We can further use the DFA<=>Category relationship as a kind of simple "composition" checker.

If the States of our DFA are types in a language, and the transitions functions mapping one type to another, then we can say that if the delta function is defined as above, and in the case there is no defined transition between some state S and some other state S', and if such a transition is called for in the delta function, then we simply send the output to a non-accepting "fail" state.


Here, the simple language consists of the following.


The Category contains:

Objects = {Int, Float, Char, Bool, Unit}
Arrows = {isZero :: Int -> Bool,
,ord :: Char -> Int
,asc :: Int -> Char
,sin :: Float -> Float
,not :: Bool -> Bool}
Values = {zero :: Int, true :: Bool,
,false :: Bool, unit :: Unit}

The corresponding DFA works something like this

f1,f2, ... fn are symbols which have type an -> bn,
where n is the same value as the nth symbol, and a and b are not type variables, eg: f1 :: Int -> Char, a1 = Int, b1 = Char
v is a type


(f1 . f2 . f3 . ... . fn) v
=> ([f1, f2, ..., fn], v)
=> [a1,b1,a2,b2, ..., an,bn,v]
=> [(init,a1),(b1,a2),(b2,a3),...,(bn,v)]


given this list of pairs, we define the DFA trace function as follows, this presumes a list like the one from above.


trace :: State -> [(Sym,Sym)] -> Bool
trace st [] = (st /= failState)
trace st [(s1,s2):syms]
| s1 /= s2 = False
| otherwise = trace (delta st (head syms)) syms


where failState is a pseudonym for whatever the magic non-accepting failure state is

and where delta simply points to the next state (be it the fail state, or otherwise). I'll cover that in more detail in my next post (I'm actually going to build this little guy for a simple language like the one above.)

I've digressed a bit from my topic, my goal was to show that Categories are really terribly neat, and apparently related to automata, which most people understand pretty easily, if they are explained well. I don't pretend to be an authority here, but hell, implementing a (very) simple type checker is a pretty cool feat, considering It was only a few months ago I started learning Haskell. I know that this isn't a robust, powerful mechanism, but as far as I know, given Compose (the (.) function in Haskell) apply (($) in Haskell) and a few other functions, you have a TC language, a la Backus' FP or FL systems.

Anyway, next time I intend to implement this little type checker, and (hopefully) eventually implement a (full) type checker for something akin to FP or FL, using this DFA style approach. Heck, I'd also be able to play with parsing (another automata rich subject).

Also, for those interesting in looking at HFA, it's available at

http://code.haskell.org/HFA/testing

you can just do a darcs get to pull everything down.




###DISCLAIMER###
I don't intend to present any of this as proven, either formally or by any other means, the ideas and conjectures in this post are just that, conjectures. Please, don't believe I'm an expert, I'm still learning about all these things, and I don't want to lead anyone down the wrong paths under the assumption I actually _know_ what I'm doing.

That said, I do think the conjectures made have some validity, if you know otherwise, please inform me. Thanks

~~Joe

20 comments:

Cale Gibbard said...

I think your definition of Category is a little off. A category has a class of objects, and for each pair (A,B) of objects, a set Hom(A,B), of arrows from A to B. (There may even be infinitely many such arrows.)

Further, if f: A -> B is an arrow in Hom(A,B), and g: B -> C is an arrow in Hom(B,C), then their composite g.f exists and is an arrow in Hom(A,C).

Additionally, for every object A, there is an arrow id_A: A -> A such that f . id_A = f and id_A . g = g for any f and g such that the composition is defined.

Also, whenever the compositions are defined, we have (f . g) . h = f . (g . h).

These laws are actually rather constraining in terms of which graph structures can actually be made into categories. The fact that compositions must be defined implies a certain kind of closure property, and that each object has at least one self-loop is also fairly constraining.

For example, if you want a single DFA to be a category, with state transitions as arrows, it must also have all compositions of state transitions as arrows as well. You'd also have to have identity arrows, which in the case of a DFA, wouldn't correspond to real transitions. So the process of turning a DFA into a category will in some sense modify its alphabet into strings on the original alphabet, add transitions on the empty string to every state, and then a transition for every composition of transitions whose symbol is the corresponding string of symbols. As a result, we could read off the language that the DFA accepts simply by collecting up the strings on each of the arrows from the start state to each of the accept states.

Another natural sort of category to form involving DFAs would be the category which has as objects all DFAs, and as arrows, has DFA-morphisms, where a DFA-morphism f:(Q,S,A,q_0,delta) -> (Q',S',A',q_0',delta'), consists of a pair of functions, f_Q: Q -> Q', assigning states of the source DFA to states of the target, and f_S: S -> S', input symbols of the source DFA to input symbols of the target, such that transitions are preserved:

delta'(f_S(s),f_Q(q)) = f_Q(delta(s,q))

initial state is preserved:

f_Q(q_0) = q_0'

and accept states are preserved:

If q is in A, then f_Q(q) is in A'.

One can form similar definitions in order to form, for example, a category of Moore machines, or a category for most any other kind of automaton.

Joe Fredette said...

Interesting, I'll definitely have to study this some more, like I said I'm no expert, but the idea popped into my head, and I figured it'd be an interesting idea to share.

I am a little confused, I think that you can still use the DFA I described towards the end as a kind of a type-checker, because it is designed to specifically deal with composition of arrows. You certainly seem to be more knowledgable about this than me. I suppose the idea is just this:

a valid function created by:
(f . g . h . i)
has a signature that looks like

a -> b
b -> c
c -> d
d -> e
or
a -> e

So if the states are the types, then the functions are arrows between types, composition is then implicitly defined, I think.

Anyway,thanks for the info.

~~Joe

Unknown said...

You might find it interesting to look up "presheaf categories". Cool things with categories are actually functors, rather than morphisms. A good place to start is http://math.ucr.edu/home/baez/week115.html

Anonymous said...

Cool website, I had not come across disparatemathematician.blogspot.com before in my searches!
Continue the excellent work!

Anonymous said...

Our company creates a subject funny man destined on the basis of harmonious ' and beautiful projects.
These projects are carried out by the cards the most outstanding staff of graphic artists and designers in
the buy who are experts in every discrimination of the word. They are also quite flexible, so you can
carry out barest interesting trade press card designs, depending on the separate needs of each client.
We do not own a whiz printing machines word of honour the highest je sais quoi of each individual card.
Deviating quote of paper allows you to upon the expectations of notwithstanding the most tough customers
from every conceivable industry. We make sure the copy and amenities of huge quantities of responsibility
cards in the shortest credible time. In our case, the highest quality is the satisfaction of the proposed
price and reliable checking from people receiving and carrying out an decree recompense task cards.
With access to the services offered as a consequence our website, you can quickly and without undue
formalities mission an degree object of goods, judgement the concoct and approved it and ordered some job
cards. Elect our coterie as a respectable subject window-card is oft a guaranty fitting for success.
Greet
Merio [url=http://www.kalendarze.dogory.pl]Kalendarze[/url]

Anonymous said...

Nice dispatch and this enter helped me alot in my college assignement. Thanks you as your information.

Anonymous said...

Sorry for my bad english. Thank you so much for your good post. Your post helped me in my college assignment, If you can provide me more details please email me.

Anonymous said...

kiev escort girls ))

Anonymous said...

[b][url=http://www.besthandbagstore.co.uk/]louis vuitton outlet[/url][/b] Next, vary your speaking speed. In a single stage of your speech, you would possibly justifiably use the rapid-fire solution Tv set viewers hear when the motor vehicle salesman races by way of a business. You do that should you have been describing a scary incident, these types of for a crime or forest fire.

[b][url=http://www.uggbootsoutletukstore.co.uk/]uggs boots outlet[/url][/b] B vitamins are certainly necessary for your body to synthesize serotonin and thus not feel depressed. Looking at that serotonin could be the major neurotransmitter involved in depression procedure (Prosac is called a Selective Serotonin Reuptake Inhibitor) and B vitamins are required to synthesize serotonin, shouldn't health professionals be supplying nutrient infusions of B nutritional vitamins ahead of placing somebody on the medicine? But dietary analysis prices income and insurance policy providers have yet to deem ample nutrient provide a worthy purpose during the disorder care process. At this time my regional mechanic appears to be smarter that our health care method.

[b][url=http://www.uggclearancewebsite.com/]ugg clearance[/url][/b] "We will not have any cash," she states. Shinichi will work in a butcher store; he is pondering quitting higher school. Norie not long ago started doing work part-time for the same butcher and earns about $675 a month. Also when you do get any Mont Blanc bogus designer handbag, you can expect to recognize and also acknowledge that how wonderful along with rewarding totes these are. Obtaining mentioned that, in case you purchase a deluxe creator Louis Vuitton reproduction females purse by a trustworthy designer purses lookup, then you can make certain just how very hot moreover tentalising designer purses they are really. Upcoming in the event that you snatch Mentor Suitcase over the web, there is usually some sort of huge minor little bit of unique and fashion inside it frequently.

[b][url=http://www.hotsalelouisvuittonstore.co.uk/]louis vuitton uk[/url][/b] Then ways to acquisition a sneakers that may overall look your frame of intellect auspiciously is surely an significant level. That is the precision that there are various manufacturer names of aerial heel footwear, but christian louboutin nude pumps continue to stands in the prime scenario amid them. As is acknowledged to us, christian louboutin sneakers is acclaimed for its enough action and diverse structure and design.

[b][url=http://www.hotsalelouisvuittonstore.co.uk/]www.hotsalelouisvuittonstore.co.uk[/url][/b] All through the planet, Nigeria might be necessary variety of an english college. For kinds wedding day, to . Take out your digital camera person guide. Inspite of its superior riding strategies, the Rav4 has become a soft-roader from its inception while in the 1990's, and designed on the car-like unibody chassis. The exterior spare served as a packaging solution and one thing of the style folly while in the times in advance of rugged SUVs started acquiring a poor rap. The Honda CR-V utilized to activity the same feature, but it really was removed within the vehicle's style and design a number of ages back..

Anonymous said...

Johnny Weissmuller (1904-1984) is perhaps the most famous of all the Olympic swimmers though it is for his role at Tarzan that he is best remembered Despite being a fixture in Washington DAll throughout history the eagle had been used as a symbol Some people are also uncomfortable wearing anything around their necks Some of the services which should be disabled are Windows Search[url=http://www.VinceWilforkJersey.net]www.VinceWilforkJersey.net[/url]
Windows Defender[url=http://www.raylewisjersey.net]www.raylewisjersey.net[/url]
Windows Cardspace[url=http://www.AntonioBrownJersey.net]Antonio Brown Jersey[/url]
and usually a number of third party tools such as HP print managers[url=http://www.russellwilsonjersey.net]www.russellwilsonjersey.net[/url]
Adobe tools[url=http://www.AndreJohnsonJerseys.net]Andre Johnson Jersey[/url]
Real player[url=http://www.AndrewLuckJerseynike.com]www.AndrewLuckJerseynike.com[/url]
MSN[url=http://www.jjwattjersey.com]jj watt womens jersey[/url]
Google toolbar[url=http://www.AldonSmithJersey.net]www.AldonSmithJersey.net[/url]
Antivirus control panels etcdittoTweetbackground: #fff;padding: 10px 12px 10px 50px;margin: 0;min-height: 48px;color: #000;font-size: 18px !important;line-height: 22px;-moz-border-radius: 5px;-webkit-border-radius: 5px; p But even if your yard is small[url=http://www.MattRyanJersey.net]Matt Ryan Jersey[/url]
there are several ways to turn it into a Mediterranean style haven
ï»?And that’s just the people who reported their injuriesWww Be wary of opaque packaging that doesn't allow you to inspect all the seedtimestamp aOne of the serious risks associated with phentermine use is addiction I know that you are wondering form where I can get those? Now I will act like a jenny coming out of the lamp to answer these questions

Anonymous said...

On another inverted coaster#file_links[D:\NFL\UBB.txt,1,L] Dueling Dragons at Universal Studios' Islands of Adventure#file_links[D:\NFL\UBB.txt,1,L] one corkscrew on the "Fire" track interlocks with the corkscrew on "Icetimestamp a > span {display: inline-block;width: 16px;background-image:url(http://images The company is also the official supplier of gloves in the NFLDo little homework before taking the plunge into world of endless fun This color will determine the ambience of the sports walls and the roommetadata div
In this case#file_links[D:\NFL\UBB.txt,1,L] you can see that these products are really great for your needs and its presence can be a good help for your needsindent { margin-left: 20px; } divBack in 1992 the FCC allocated the 2Director: Don Siegel Review: "In its own small way#file_links[D:\NFL\UBB.txt,1,L] Riot in Cell Block 11 is a realistic and effective combination of brawn#file_links[D:\NFL\UBB.txt,1,L] brains and heart Note: Add guidelines to your project that don't get printed Although it was business as mainstream#file_links[D:\NFL\UBB.txt,1,L] but its essence remains parallel Communicate with all teams to explain the reasoning for assigning tasks using costbenefit analysis#file_links[D:\NFL\UBB.txt,1,L] if appropriate#file_links[D:\NFL\UBB.txt,1,L] to prevent illfeeling between teams

Anonymous said...

Hello. Facebook takes a [url=http://www.onlinecraps.gd]slots online[/url] stake on 888 casino freight: Facebook is expanding its efforts to the moment real-money gaming to millions of British users after announcing a wrestle with with the online gambling companions 888 Holdings.And Bye.

Anonymous said...

top [url=http://www.c-online-casino.co.uk/]c-online-casino.co.uk[/url] hinder the latest [url=http://www.casinolasvegass.com/]las vegas casino[/url] manumitted no set aside reward at the chief [url=http://www.baywatchcasino.com/]casino perk
[/url].

Anonymous said...

4 2011 he vaulted past Britney Spears in the Most Twitter Followers category.
For example, I have added about 3000 followers and 1000 people have followed back.
but most importantly, the content you share should be the ones that are most valuable and most relevant to
your network.

Stop by my webpage Buy cheap Twitter Followers

Anonymous said...

Now this should be done carefully as different Xbox games offers different amount of free codes.
Totally free xbox live codes are also given
by some console sellers as being a definite incentive on buying Ps3 live.

Another way to earn free Xbox codes is by competing in
the competitions that are held up by Microsoft.

Anonymous said...

[url=http://longchampsoldesk.quebecblogue.com/]longchamp soldes[/url] I have 3 PPB bags. Cross Town Clutch, Touring Tote and a Society Satchel! I LOVE them all and they all serve a different purpose. Clutch is good for dinner out or small outing, tote Online Cheapest Mulberry Dan Nautral Leather Messenger Bag Brown for Men,Our Mulberry outlet store is one of the best Mulberry outlet online. is kind of like a hobo bag but with structure and holds a decent amount and the satchel is big enough for travel and is a beautiful bag that doesn't look like a diaper bag..
[url=http://quizilla.teennick.com/user/longchampsoldesa/journal/]longchamp soldes[/url] Express milk on one breast while your baby is latched on the other Shop the Mulberry bags at our online store, Crafted Mulberry Zip Around Slim Natural Leather Purse Light Coffee for Women sale online breast. If you have twins, you may breastfeed at the same time. If you have one nursing child, you can stimulate more milk production by letting your body feel that you are nursing twins.
[url=http://longchampmoinse.bloguez.com/]sac longchamp[/url] I have two Tom Bihn bags for sale. My wife and I are looking to start traveling very light and are getting new Synapses, so we need to get rid of our old bags. Ristretto for iPad.. I don't always answer every single question, but I find that they help me explore and record the memories of the past month in a simple and concise way. Sometimes I answer the roundup questions with a bullet list, and other times I may write a paragraph or even more explaining the events that occurred. There is no Exclusive Mulberry Outlet Medium Alexa Leather Satchel Black Bags scored its first high-fashion success "right" or "wrong" way to do a roundup, just try to include as much detail as you want to remember. Orange and PoliticsThe town of Orange in Provence in the south of France was originally nothing to do with fruit. The original Roman name of Arausio dates from before oranges were introduced into Europe. The name was gradually changed from Arausio into Orange and this change was probably influenced by the name of the fruit trees which grow in the south of France...

Anonymous said...

It is caused by the hormonal problems, weight gain,
and many other factors. It contains natural ingredients like olive oil,
jojoba oil, and other essential oils. Vichy is a very popular company in
the European market.

Here is my weblog :: Cellulite removal

Anonymous said...

Then it is important to apply general amount involving any medical cream like Clearasil on your own face.
As a word of caution you should also never try to manually remove the warts yourself, as
that can lead to the virus spreading. There are a wide range of self tanners to choose from at department stores,
but why not treat yourself to a spray tan at
your nearest tanning salon.

my blog post: how to get rid of warts and moles

Anonymous said...

It's strictly the get back your ex girlfriend drink for two full weeks. I am going to need energy and that energy comes from food. It's effectivity in breaking down built
up toxins in the human body. Designed by New York cardiologist and get back your ex girlfriendification specialist Dr.

Good News Sauna is one of the medicinal herbs used for cleansing liver.
Lymph get back your ex girlfriend herb: Cleavers is one of the other choices
that you can drink it.

Feel free to visit my homepage ... web site

Anonymous said...

Moreover, the right posture makes you look taller instantly.
The functions of your body will be accelerated so
that what is working will work better than before.
In case you are flexible like me you'll want to fully grab your ankles to achieve the maximum stretch.

My site grow taller