Jonathan Bryant watersofoblivion

CFA and the State Explosion Problem

I've read (among other things) both Shiver's dissertation on CFA and Might's dissertation on extending CFA, as well as Might's m-CFA paper. In Shiver's dissertation, he gets the naive exponential CFA down to polynomial by using the single-threaded store. In Might's dissertation, he extend this with various analyses on CFA environments, such as Gamma CFA where you garbage collect dead elements of the environment to reduce processing time. Then, in the m-CFA paper, he shows that you can actually produce a family of polynomial CFA algorithms by using what is tantamount to flat closure conversion instead of linked closure conversion.

The running theme here seems to be that CFA has the state explosion problem and memory management is crucial to the runtime of any CFA analysis. So much so that it can actually

	# Rails Application Template
	#
	# My personal template for Rails applications. Does a few things:
	# - A few odds and ends (public/index.html, README => README.rdoc, etc.)
	# - Sets up Rspec
	# - Sets up Cucumber
	# - Sets up Selenium
	# - Stuffs everything into a git repository
	# - Creates a project on Heroku and pushes the repo there

	@import <Foundation/CPObject.j>

	@implementation Model : CPObject
	{
	CPString foo @accessors;
	CPString bar @accessors;
	}

	@end

	/-
	# Question on Inductively Defined Propositions

	I've hit a brick wall while learning Theorem Proving/Dependent Types, and that
	brick wall is Inductively Defined Predicates. There's something about them
	that I'm not fully grokking, and I don't understand what I don't understand
	well enough to articulate what I'm not getting.

	I've finally found a (relatively) small example that illustrates the issue I'm
	having in a way that someone can hopefully "fill in the blanks" as a jumping