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 · h2and 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 |- Pwhere 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 /\ QThe 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

Edit | Attach | Print version | History: r2 < r1 | Backlinks | Raw View | Raw edit | More topic actions

Topic revision: r2 - 10 Jul 2009 - 00:00:36 - DavidAspinall

Copyright © 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

Ideas, requests, problems regarding TWiki? Send feedback

This Wiki uses Cookies