I thought I’d scribble a few things down while they’re fresh in my mind. First up, we’re shifting to Tuesday afternoons from next week, to give me time to get here from another country…
The eagle-eyed will have spotted a bit of darcs activity from myself and James C of late, so I painted some of the picture about the new proof state structure, replacing the OLEG-based system we had before.
It’s a bit slippery if you’re not used to it. Here’s the basic grammar:
- thing ::= decl | defn
- decl ::= uid : ↓term
- defn ::= uid [thing;*] => status : ↓term
- status ::= # | ? | ↓term
OK, some explanation is in order. A thing is either a (male) decl or a (female) defn. The hierarchical structure comes from the way a defn contains a sequence of things, her children. The whole proof state is (morally) a boring defn called root, with interesting children.
There is a certain subtlety in the relationship between the display form of a proof state and its internal form. The internal form uses absolute names which trace the maternal line from root. Moreover, Edwin will be disappointed to learn that internally, each definition is fully λ-lifted over all the parameters in whose scope she sits. Rotten luck, old chap. Meanwhile, the display form uses relative naming and treats each definition as if it were local to those parameters shared by the reference and the referring term. That is, the display name and the effective type of a definition vary, depending on where you are when you refer to her. Confused? OK,
root [
h [y : T] => ? : T
f [
x : S
g => t : T
] => h (h g) : T
s => ? : S
t => f.g s : T
] => () : One
So, in the term defining f, g appears to have type T, because parameter x has both g and f’s body in his scope. However, by the time we come to define t, we are obliged to refer to the same thing as f.g and to instantiate x explicitly.
We support working mothers. Each definition has a value in her own right, but is also the mother of her ‘module’ of daughters. These modules are not first class, hence there is no ambiguity: a definition’s name always means her value. Syntactically, f.g is the name of a daughter, not the application of a projection operator. This ‘module system’ seems vaguely related to the Agda II system of parametrised modules as outlined by Ulf the other day. This plan with the working mothers may shed some light on my remarks at that (rather splendid) virtual meeting about definitions doubling as the modules of their subdefinitions.
Meanwhile, for LEGO old-timers, what we’ve done is to turn ‘Discharge’ from a temporal operation (a definition is local until you discharge her parameters) to a spatial one (a thing is lifted over her out-of-scope parameters). Internally, they’re fully lifted, but James C and I knocked off the lump of code which generates the localised display forms from these things yesterday evening. Coqueurs will doubtless recognize Dowek’s ‘sections’, but here we support the spatial editing of sections, rather than temporal operations which open and close them.
Relative to OLEG, what’s new is that the notion of ‘guess’ has vanished. A definition’s daughters (et ceterae) are in scope for her younger siblings, with names lengthened by a matronymic and parameters corresponding to their discharged elder brothers. Where we used to work locally inside a guess, then λ-lift and export the subobjects from inside the guess to before it, in order to bring them into scope and turn the guess into a definition, we no longer need to: they’re already λ-lifted and they’re already in scope!
Lessons learned from Epigram 1:
- Retain syntactic representations of all components. Perform updates on the syntax, then regenerate the semantics if and when things change.
- You don’t need to duplicate the parameters of a bunch of definitions or flatten the family tree in order to lift-and-export them.
- By keeping the tree structure and book-keeping dependencies, cheap tests can allow updates to flow only where they’re needed.
Next steps:
- Provide a simple navigation mechanism for the proof state (which we represent as a maternal-line zipper, natch).
- Allow typechecked definitions to be inserted at any point.
- Allow a baby boy only if mum is still functional.
- Allow the status of a definition to change by filling a hole or undoing it.
- Implement the commit mechanism to regenerate a definition reference from its proof state entry and propagate the changes (either progress or regress).
Once we have that, the serious tactic-writing can begin…