Christoph and David discussed adding meta-variables on 2.7.09. Some remaks/questions:
- Why do we want to do this?
- presumably: to explain operational behaviour, including "action at a distance" (i.e. instantiating a variable in one branch of the proof affects other places where it may appear)
- The present formalisation treats meta-variables as an implementation detail; when instantiating an unknown (eg. the witness in the exI-rule), one has to give the complete instantiation at the point of the rule application.
- Is it necessary?
- The "action at a distance" effect breaks the congruence rules for the tensor. It is unclear how to recover the existing proofs. Do we still want congruence in the big-step sematnics?
- A first suggestion was to use a monoidal structure on the goals rather than the free monoid (aka lists). Mathematically, this looks nice in the tensor rule
g1 |> t1 ==> s1 <| h1
g2 |> t2 ==> s2 <| h2
-----------------------------
g1 · g2 |> t1 (x) t2 ==> s1 (x) s2 <| h1 · h2
and then the action · of the goals monoid can encode things like "unify and instantiate meta-variables". However, this threatens to break the semantics because now we can't distinguish single goals from multiple goals anymore.
- We can encode meta-variables in the judgements of the underlying logic. Example (for the simple fragment of propositional logic).
Judgements come with a context, and a set of meta-variables i.e.
\Gamma, X |- P
where X is a set of variables, together with their instantiations. Rules with more than one premise need to unify the meta-variables and their instantiations:
\Gamma, X |- P
\Gamma, Y |- Q
-------------------------------------------
\Gamma, unify X Y |- P /\ Q
The problem here is that this, just like the formalisation we have at the moment, does not explain the "action at a distance" effect
- Maybe parametrisation on goals can help?
Here is a tactic to duplicate goals using lambda-abstraction over goals:
\lambda x:g. (x; a) \otimes (x; a)
Problem with this is the typing-- above, it does not make much sense to abstract over a goal g if all you can instantiate it with is g.
--
ChristophLueth - 2009-07-03