?

Log in

No account? Create an account
"Efficient representations for triangular substitutions: A comparison in miniKanren" - Lindsey Kuper [entries|archive|friends|userinfo]
Lindsey Kuper

[ website | composition.al ]
[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

"Efficient representations for triangular substitutions: A comparison in miniKanren" [Oct. 28th, 2009|01:58 am]
Lindsey Kuper
[Tags|]

My colleague Dave and I are writing our butts off so we can submit a paper to FLOPS 2010! Here's the abstract, which I just turned in:

Unification, a fundamental process for logic programming systems, relies on the ability to efficiently look up values of variables in a substitution. Triangular substitutions, which allow associations to values that are themselves bound by another association, are an attractive choice for purely functional implementations of logic programming systems because of their fast extension time and linear space requirement, but have the disadvantage of costly lookup. We present several representations for triangular substitutions that decrease the cost of lookup to linear or logarithmic time in the size of the substitution while maintaining most of their desirable properties. In particular, we show that triangular substitutions can be represented efficiently using deferred-extension skew binary random access lists, and that this representation provides a significant decrease in running time for existing programs written in miniKanren, a declarative logic programming system implemented in a pure functional subset of Scheme.

Yep, that says "deferred-extension skew binary random access lists". Best data structure ever! It's hilarious how I write about stuff like this, and then I go to job interviews and can't answer questions about hash tables.

LinkReply

Comments:
From: catamorphism
2009-10-28 04:12 pm (UTC)
It's hilarious how I write about stuff like this, and then I go to job interviews and can't answer questions about hash tables.

Yeah, I think that's usually how it goes. Shameful secret: I didn't even really know what a hash table *was* until I had a master's degree in CS.
(Reply) (Thread)
[User Picture]From: lindseykuper
2009-10-29 04:59 am (UTC)
I remember having a conversation with Jesse jes5199 a couple of years ago in which I was telling him all the things I didn't really learn in undergrad.

Jes: Well, what did they teach you, then?!
Lindsey: Um...the pumping lemma.
Jes: What's that?
Lindsey: ...I don't remember.

Awesome, just awesome.

Edited at 2009-10-29 05:00 am (UTC)
(Reply) (Parent) (Thread)
From: catamorphism
2009-10-29 04:14 pm (UTC)
I get the feeling nobody really thinks much about the pumping lemma (I almost wrote "pumpkin lemma", ftw) until they get to be a professor and it's *their* turn to torment the undergrads with it.
(Reply) (Parent) (Thread)
From: (Anonymous)
2010-01-16 07:23 am (UTC)

Awesome indeed.

Sigh. You know, I'm teaching the automata theory course again in spring 2011. You're sapping my motivation.

OK, I'll make this as quick and easy. The pumping lemma is a way to show that a set of strings isn't a regular language. Imagine it as a game between two players, Con and Pro, who disagree about a set L of strings. Con wants to show that it's not a regular language; Pro wants to keep alive the possibility that it might be regular. The game that they play is a short one, only four moves: (1) Pro chooses a positive integer, p. (2) Con chooses a string s that is in L and is at least p symbols long. (If Con can't find such a string, she loses, because then L is finite and all finite languages are regular.) (3) Pro partitions s into three substrings uvw, where v is not the null string and the sum of the lengths of uv is less than or equal to p. (4) Con chooses a non-negative integer n, the repetition factor. Now the players check whether the string formed by concatenating u, n repetitions of v, and w is in L. If so, Pro wins; if not Con wins.

The pumping lemma says that if L is a regular language, then there is a winning strategy for Pro. The proof just explains what that strategy is: Build a deterministic finite automaton M that recognizes L and choose p as the number of states in M. In processing the string s, the automaton makes p transitions, so at some point it has to re-enter a state that it was in previously; choose the substring v as the substring processed after the automaton entered the repeated state for the first time and before it exited from it the second time. Since M accepts uvw, it will also accept u v^n w -- for the middle part, it will just run through the cycle of states n times.

So if, on the contrary, there is a winning strategy for Con, L can't be regular. Thus you can prove that a language isn't regular by finding a winning strategy for Con.

There's also a pumping lemma for context-free languages, which differs only in the way move (3) works -- Pro has to partition the string into five substrings, uvwxy, such that not both v and x are null and the sum of the lengths of v, w, and x is less than or equal to p. The proof of the lemma is different, of course, but it too is quite elegant -- go back and look it up if you don't believe me.

This is not torture, friends. This is enlightenment.

John David Stone
(Reply) (Parent) (Thread)
[User Picture]From: pmb
2010-01-16 07:48 am (UTC)

Re: Awesome indeed.

This is not torture, friends. This is enlightenment.

Preach on.
(Reply) (Parent) (Thread)
(Deleted comment)
[User Picture]From: lindseykuper
2009-10-29 04:52 am (UTC)
*flips through*

Chain pruning aka path compression? Actually, we do (but without side-effecting the substitution -- we just stick the last thing in the chain on the front of the substitution so it's faster to look up the next time). (Does path compression come from Cardelli? If so, awesome -- I was looking for an appropriate reference.)

We have a couple of other tricks for dealing with long chains, as well, but part of the gist of our paper is that we find that most of the substitutions that arise from running real miniKanren programs don't contain very long chains; rather, they're just big. So, we present some techniques that make real mK programs run faster. (Although our suite of "real" mK programs includes, you know, the Zebra Puzzle, so I guess "real" is debatable.)

Would you be interested in looking over the paper? I'd love to get comments from you (in a couple of days, probably, once I finish making all the revisions that are already on my list).
(Reply) (Parent) (Thread)
(Deleted comment)
[User Picture]From: lindseykuper
2009-10-30 07:19 am (UTC)
Great! I'll get it to you.
(Reply) (Parent) (Thread)
(Deleted comment)
(Deleted comment)
From: (Anonymous)
2009-10-30 04:14 pm (UTC)
> By chain pruning I mean...

Hee. I love how reading this journal always gives me great tips for my own thesis... about a month or so after I've learned about the same principle the hard way.
(Reply) (Parent) (Thread)
[User Picture]From: stereotype441
2009-10-29 02:50 pm (UTC)
I want to read that paper.
(Reply) (Thread)
[User Picture]From: lindseykuper
2009-10-29 09:55 pm (UTC)
I want you to! I'll send you a draft of it in a day or so.
(Reply) (Parent) (Thread)