Date: Tue, 23 May 2006 10:47:06 -0500 From: Sol Swords Subject: Meeting tomorrow Hi all, I'll be talking at tomorrow's ACL2 meeting, which is at the usual time and place: 3.116 ACES, 4:00. After that, the tentative plan is to meet again on June 7 and subsequently on June 21. However, if you would like to speak or know of someone who would like to speak, please let me know; we have the room reserved for the intervening Wednesdays as well so those dates are also fine. I'll be discussing the disjoint set union-find problem and a solution I coded up for it in ACL2 for use with the transistor-level analysis system I've been working on with David and Warren. Using the hash-table-backed alists provided by Warren and Bob's modified version of ACL2, we can obtain O(n alpha(n))-time performance which is known to be a lower bound for this problem. The main challenge in the implementation was admitting the recursive alist traversal operations without allowing termination-related computations to affect the performance of the algorithm. In the talk, I'll focus on describing the termination argument I ended up using. - Sol