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

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.


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)