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