finis

Hey, we're done.

Added conclusions

I've added a short conclusions section. See what you think and if you can fill in the missing citation.

Also, getting our names on this paper might be nice.

I've taken care of all the high-priority items left, I'm happy to have it turned in pretty much as-is if you have no further issues with my section. So I'm leaving it alone until you tell me something needs fixing.

--Carl

deltas to termpaper.*

Just so you know, I'll be making changes throughout the day today. I did some changes to Carl's section this morning; I'm probably going to focus on my section and the introduction for what remaining time I spend on this.

Please try to:

1. look at svn diff's
2. look at the log
3. finish your section
4. write a (smallish) conclusion.

Sometimes I'll be putting margin notes in (when I want to push a topic onto you to be sure it gets accounted for), but for the most part I'll be putting thoughts and commentary into the svn log. Since I may make changes to stuff in your area, its important that you sanity check those changes. Thus, svn diff, si vous plait!

I'll try to flesh out the introduction some more. But I'd like your feedback on whats already there. I'm trying to figure out how I would justify the study of type theory to the average algorithmicist, automata theoretician, or programmer.

tyeps, type constraint systems, strings, etc

I'll be checking in my notes shortly, but I figured that this wasn't going to fit into a margin...

In section 10.2, you discuss the correspondence between type constraint systems and non-deterministic finite automata.

It seemed from my reading that a type can be read as a (potentially infinite) tree, which in turn can be read as the set of strings that describe all paths from the root to the leaves of the tree. Thus, a type corresponds to a set of strings, or a single language.

In section 10.2, you say that there is a correspondence between type constraint systems and NFAs. But to me, a type constraint system describes not just one type, but rather a (potentially empty) set of types. Therefore, a type constraint system (TCS) corresponds to a set of languages, while an NFA corresponds to a single language.

Can you resolve this confusion for me (preferably by amending the paper with some sort of clarifying note)?

feedback

Okay, I spent an hour or so going back over the paper, trying to put special focus on the new additions on Recursive Subtype Constraint Entailment.

I was pretty happy with most of what I read (or maybe I'm just desparate to declare this thing finished), but I found myself going back over section 10.1 several times because I was confused by two things that looked like distinct conflicting "definitions" for the subtyping relation, <:

At one point, there is a line "The subtyping relation on T_Sigma is defined as follows. t <: t' iff ..."
and later there is the paragraph on Nonstructural subtyping which fixes Sigma = { \times, \to, \top, \bot } with latice ordering \bot <: \sigma, \sigma <: \top for all \sigma in \Sigma.

Did you mean to use the same "<:" in both places? Or are the second set of "<:"'s really analogous to the <:_B base type relation (or perhaps I should be calling it <:_\Sigma here)? I was confused by that, but ended up deciding that you must have not intended for the two notations to collide.

There are other changes to suggest, but they are merely suggestions or minor details, so I'll either make them directly myself or add "margin notes" for them.

Finished preliminaries on recursive subtyping.

I have finished writing up (and will momentarily commit) the preliminaries to the section on recursive subtype entailment - the next thing to be added will be the "meat" of the reduction from a PSPACE-complete problem. It bothers me to discover that the problem is established as PSPACE-complete in "personal communications" with the authors, but if they were willing to publish that then we can report it.

The "other" two systems presented in this paper are slight modifications on the original and based on the same reduction and automata equivalence. I think after presenting one it should be sufficient to merely mention the others, and get around to cleaning up the presentation and transitions in our papers. I should be able to finish the bulk of the material tomorrow (Tuesday), leaving us some time to polish it depending on when you want to hand in by.

Let me know what schedule works for you. I can put in more time tomorrow while other Santa Barbara folks are working if you're worried about pushing too close to the "end of the month" deadline, but I figured Thursday or Friday would be fine for submission.

--Carl

Moving on: Recursive subtyping

I began the recursive subtyping section with a motivation of and definition of constraint entailment, then began a description of the type system involved. Some of the definitions will be repeats of the foundations at the top of the paper - there's some overlap in the selftype section too. We can fix that up as we go, it's easier just to lay out what I want to say as I say it for now.

Felix, let me know if there's more work I need to be doing on selftypes first, but it looked technically complete enough to start work on the next paper.

--Carl

Tuesday work

I tightened up some of the explanations of the restrictions on grammars and the explanations about types and grammars. I also put in real ellipsis notations some places it was missing and changed the constraint forms figure to show grammar productions.

I'll be getting up early tomorrow morning to move my car, I'll put in an hour or two before work.

Starting cleanup

I very hastily closed off the technical discussion in my section, then went through and addressed all but one of our margin notes. The last margin note says things are very "hand-wavy", and they are. The next step will be to stop waving my hands and to point at some real details.