-
Notifications
You must be signed in to change notification settings - Fork 5
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Translation of nameless proofs to named proofs using proven alpha-renaming? #362
Comments
The idea of using pattern hashes for fresh variable names and the focus on the "rules". So you're saying that this local view could let us ignore thinks like commutativity of Two other comments:
If it means that you simply subtitute For example, Just an idea: maybe what would work is bottom-to-top with decrementing on other indices like But I might just not understand De Bruijn indices because I never worked with them :-)
|
Yes, the main idea here is that the nameless proof system is more powerful because it reasons modulo alpha-equivalence. We may therefore need to use more complex proofs in the named version to recover this. Alpha-equivalence is not something that is "built into" the named proof system, but rather something that must be proved.
Commutativity of
That's a good point. I think
I wasn't really sure what the correct notation for naming a variable in a nameless pattern is and just made one up. |
I started implementing @nishantjr proofs from above with the named proof system in Coq. However, I found that the axioms
To show that the equality above does not hold, we can use the following instances of the metavariables:
With these instances, we simplify the definition of substitutions.
Therefore
I think, the same train of thoughts also applies for the provability of There were no issues with the existential case, because the axioms can be derived for renaming. |
@berpeti I'm not sure if I've understood things fully, but if If so we should discuss replacing these rules. |
I double-checked the Metamath formalization of The first proposition is proved by the axiom
That is, |
I see. That makes sense. The problem is that There are two directions we can take:
In either case, my feeling is that
from the current:
In the original notation:
For context, this is the current rule.
|
Actually, this issue is not specific to only I do not think, it is a good decision to change |
Thanks for the explanation. That makes a lot of sense.
I don't understand what It seems that in the metamath formalization Lets discuss this is detail in the meeting next week. |
Renaming is defined by a function, just like the substitution. It is basically a special substitution that replaces a variable with a variable. In Metamath I think, it is not needed to find exactly the variable specified in either of the definitions. The important bits are the side conditions of (1) and (2) that need to be captured, and the variable
I agree. |
I'm not convinced that there exists a naming scheme for variables that meets all
5 requirements in the report. This is because in the nameless representation we
are reasoning modulo alpha-equivalence and is therefore more powerful than the
named one. My suspicion is that proofs the make copies of patterns (e.g. KT) may
cause problems. I've not tried too hard to come up with a counter-example
though.
In particular, does there will always exist a direct (without some
alpha-renaming) translation of the proofs from nameless to named? Even if it is
possible, it looks trick and complex. Could we avoid the problem entirely?
One way to do this is to use a less direct translation, using proven
alpha-equivalence at certain points, allowing us to drop requirement 3. For
now, let us ignore metavariables and return to them later.
I hope I've not oversimplified things, and completely underestimated the problem.
Requirements
In order to translate proofs it is sufficient to have a translation
function
t: NamelessPattern -> NamedPattern
, such that for any nameless proof rule,there is a named proof rule or theorem, such that
Further, we need that:
so that we can translate proofs from the nameless to the named representation.
Candidate function for
t
Let us define a stateless translation function,
t: NamelessPattern -> NamedPattern
.Let
n_e: NamelessPattern -> EVar
andn_s: NamelessPattern -> SVar
be injective functions,e.g. returning a unique string representation of each distinct pattern.
Define:
All other patterns are translated in the obvious way.
For axioms that do not deconstruct binders as well as (ex-quan), (ex-gen),
it is clear that
t
meets our requirements.This leaves us with (prop-ex-*), (pre-fixedpoint), and (knaster-tarski).
that do not fulfill (ERASURE). Let us prove alpha-renamed versions of these.
Conveniently, for any named pattern phi we have:
when
x
is fresh in phi.Using the Metamath proof rules we can also prove that:
when
x
is fresh in phi.This allows us to prove an alpha-renamed versions of (prop-ex-*), (pre-fixedpoint), and (knaster-tarski)
that do fulfill (ERASURE).
(TODO: Paper proofs are in the final section, but I've not tried mechanizing these yet, so there may be errors.)
This technique should also work for axioms applied using the (hypothesis) proof rule in Coq, and for translating theorem statements and hypothesis, through congruence-of-equivalence theorems (Proposition 44 in the 2019 TR).
Dealing with metavariables.
We already have the metamath axioms (where ==> and <===> respresent provability in the
#Substitution
relation):substitution-identity
:phi[x/x] ==> phi
substitution-fold
,substitution-unfold
:phi[x/y][psi/x] <===> phi[psi/y]
ifx
is fresh inphi
I think we may additionally need:
substitution-comm
:phi[x1/y1][x2/y2] ==> phi[x2/y2][x1/y1]
if distinct(x1, x2, y1, y2) andx1
,x2
is fresh inphi
While this is a meta-theorem, I feel that this is a reasonable axiom to add,
since it only talks about the meta-operation substitution and is only needed for metavariables,
if it lets us move forward with the MM translation.
I feel that we need to strike a balance between practicality and purity and if this axiom or similar ones
are needed to respresent, or significantly shorten some meta-ish proofs in Metamath it is worth it.
In the long run, as Xiaohong had mentioned, we can have a meta-level representation of matching logic's
proof system itself to encode these theorems if necessary.
Alpha renaming in MM
We start from the goals and work backward.
Proof of
(exists x phi[x/y]) <-> (exists y phi)
whenx
is fresh in phi.Proof of
(mu x phi[x/y]) <-> (mu y phi)
when x in fresh in phi.The text was updated successfully, but these errors were encountered: