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

Topic revision: r2 - 10 Jul 2009 - 00:00:36 - DavidAspinall
 
This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback
This Wiki uses Cookies