redprl / sml-dependent-lcf Goto Github PK

Maybe there is already one but I did not find it...

I want to try out alternative representations of the proof that that would avoid premature substitutions; but to do this, I need to somehow make the proof state abstract so that it is feasible to integrate the experiment with RedPRL.

The idea would be that we would expose the current version of the proof state in certain parts of the interface (such as in the interface for rules).

One problem with the current, fully-syntactic approach is that it's not possible to do anything with the syntheses of subgoals in the synthesis of the main goal except put them somewhere. This rules out "admissible rules", but even worse, it makes it impossible to do something like substitute a variable in one of the sub-syntheses.

The proper solution to this problem is not yet clear to me, but I wanted to record it here. I'm loath to switch back to full HOAS for everything, since it will make the implementation a zillion times more complex.

This idea was spawned in the course of developing the denotational semantics for Dependent LCF—I realized that the naturality condition which I imposed prevents any "interesting" validations from being written which are not equivalent to just open terms with free metavariables in them. So we might as well switch to that representation, since it will be a bit simpler...

RedPRL/sml-redprl#592

Developing the denotational semantics of Dependent LCF has clarified things greatly, and now I know that the thing implemented here is not a monad, much less the "right" monad. It is, however, implementable in terms of the right thing.

The correct way to do Dependent LCF is given in this snippet: https://gist.github.com/jonsterling/6a8dfc6a36e5d6284d3d8204c7285de1

It is very simple! And there is no need for the relative monad apparatus here.

We found that backtracking was basically useless in practice for RedPRL, because the state space would just blow up. I'm thinking that it actually may be a bad idea, and that in cases where we think we need backtracking, what we really need is to redesign the proof theory.

This can make use of the following things I've developed tonight:

• unification for ABTs (only renamings of metavariables needed/supported at the moment)
• alpha-respecting "subtelescope" relation

Then, suppose the goal is J. Then, if the new subgoals are a telescope T such that [x:J] <: T for some fresh metavariable x, then we have not made progress, and the tactical should fail.

Note: we can't just search the telescope for exactly J, since the metavariables/holes may have been renamed by the tactic.

In RedPRL, we implement our own generic judgment, but it is pretty gnarly; it occurs to me that it might be sensible to actually have that be a built-in feature.

This is to create an auto tactic that repeatedly applies the auto-step tactic in a certain range. So far these ranges are needed:

• apply tac to everything before n
• apply tac to everything after n

• relative monads
• category of containers
• telescopes
• logical signature == container Valence :> Sort, with a distinguished sort jdg of judgments
• category of logical signatures
• functor J from a logical signature L to the set of L-judgments
• functor T from a logical signature L to the set of proof states for L
• show that T is a relative monad on J

Perhaps we can allow a rule to attach string option something option to each subgoal.

I think that we should just use Dependent LCF from the start; I think it's ready, and it will be easier than if we have to rewrite the refiner again, which I worry wouldn't even happy until "Crimson JonPRL" or whatever we call it, haha...

https://github.com/jonsterling/sml-dependent-lcf

The first step would probably be to switch our tactic elaborator over to target the Dependent LCF interface; this will be a minor change, since the interface is not so different from Classic LCF.

Right now, we use 'simultaneous' sequencing which has nice equational properties (it is the kleisli extension to the tactic monad). But in practice, I've found that we actually want to use the old 'sequential' one that I had hacked up originally. This one runs a tactic on a goal, performs a substitutions, runs the next thing, etc. The one we do now runs them all simultaneously, and then squishes everything.

It's kind of funny...

The example demonstrates dependency, but in a silly / confusing way. Should replace this with something like a refiner for first order logic, or a little dependent type theory.

Based on experience with other LCF implementations, I would expect to get an error when providing the wrong number of tactics for the current number of goals. Is this intentional?

I don't think there's any need for environments to be ordered... So we might improve performance by being able to switch to something like a splay dict or something.

Currently there is a some gnarliness in Nominal LCF and its use, which stems from the fact that several of its operations are in "tactic"-land, but really should be in "multitactic"-land. An example is recursion...

I think that every primitive of Nominal LCF should be considered a multitactic, and then separately these can be converted into tactics by precomposition with the unit. This approach should simplify a number of things, and will clear away some of the gnarliness.