Nominal renaming

[Todd Wilson]

Under what circumstances will a theorem of the form

forall G E F, nabla x y, {G, f x x |- g (E x) (F x)} -> {G, f x y |- g (E x) (F y)}

be true? One such case is given in examples/misc/copy, but how general is this? Are there potential nominal-manipulation tactics besides `inst` and `permute` that are admissible but currently only provable in specific instances? In other words, how complete are the current nominal-manipulation tactics?

[Dale Miller]

Dear Todd,

This is an interesting question.

On Wednesday, September 15, 2021 at 3:09:03 AM UTC+2 lambdaca...@gmail.com wrote:

Under what circumstances will a theorem of the form

forall G E F, nabla x y, {G, f x x |- g (E x) (F x)} -> {G, f x y |- g (E x) (F y)}

be true? One such case is given in examples/misc/copy, but how general is this?

This formula (with its quantification over G E F) should not be provable in Abella.  In particular, assume that G contains the formula

(pi X\ g X X :- f X X).

and let E and F be simply (w\w).  The formula

nabla x y, {G, f x x |- g x x} -> {G, f x y |- g x y}

is not provable.

On the contrary, the converse of what you asked about should be provable.  That is,

forall G E F, nabla x y, {G, f x y |- g (E x) (F y)} -> {G, f x x |- g (E x) (F x)}

should be true but not provable with the current set of tactics.

 

Are there potential nominal-manipulation tactics besides `inst` and `permute` that are admissible but currently only provable in specific instances? In other words, how complete are the current nominal-manipulation tactics?

As this converse suggests, the current set of tactics is not complete.

One way that we might make this system more complete is to replace the tactic

permute (Z1 Z2 ... Zn) <HYP NAME>.

with, say,

map (Z1 Z2 ... Zn) <HYP NAME>.

Here, we do not assume that Z1 Z2 ... Zn is a permutation.  This list could be just any (type preserving) mapping from nominals to nominals.  Mapping x and y both to x is sound and needed in this example.

Actually, we could incorporate into map the inst command as well since the Zi's could be substitution terms as well.

Probably we should explore changes to inst and perm to allow for much more general substitutions to be applied to nominal judgments around {|-} judgments.

Does such a generalization to tactics make them complete?  I'm not sure.  Maybe others have a sense of this completeness question.

 

Best regards, Dale

[Todd Wilson]

Thanks for this information, although I think that one part of it is incorrect:

On Wednesday, September 15, 2021 at 1:13:11 AM UTC-7 dale.a...@gmail.com wrote:

On the contrary, the converse of what you asked about should be provable.  That is,

forall G E F, nabla x y, {G, f x y |- g (E x) (F y)} -> {G, f x x |- g (E x) (F x)}

should be true but not provable with the current set of tactics.

You can prove this by instantiating y to be x, at least in the current implementation:

Kind i type.                                                                           

Type f  i -> i -> o.

Type g  i -> i -> o.

Theorem test : forall G E F, nabla x y, {G, f x y |- g (E x) (F y)} -> {G, f x x |- g (E x) (F x)}.

intros. inst H2 with n2 = n1. search.

The main theorem in examples/misc/copy proves one direction (the `copy_align` theorem) this way with an `inst`, and the other direction (the `copy2_align` theorem) using an induction. Part of my question was about how general the induction technique is: it doesn't seem to depend on much, even if it is not universally valid. And I'm interested in hearing what others have to say about the second part of my question concerning "completeness".

I should add that this kind of theorem comes up all the time when proving the correctness of an elaboration that simulates some constructors (like `let`) in terms of others (like 'lam` and `ap`), when f is usually the same as g and represents the simulation relation. The terms in the first argument of f are from the whole system and the terms from the second argument are from the subset. In the rules defining f, you have the choice when descending under binders between, e.g.,

f (lam E) (lam E') :- pi x\ f x x => f (E x) (E' x).

and

f (lam E) (lam E') :- pi x\ pi y\ f x y => f (E x) (E' y).

The second choice makes it easy to show that the relation is preserved under substitution, since you can instantiate x and y independently, but has the disadvantage that, during lifting, instances of x will appear in the E' terms, and you have to prove a strengthening lemma to show that these occurrences can't actually happen (i.e., that, more or less, the x's only appear in the first argument and the y's only appear in the second). The first choice eliminates this problem, but then you can't handle independent substitutions, unless you prove a lemma like the one I was originally asking about.

As a side question, if anyone has some successful experience navigating these issues to prove elaborations or simulations between systems, I'd be interested in seeing how you did it.

--Todd

[Dale Miller]

Dear Todd,

Thanks for this information, although I think that one part of it is incorrect: 

Thanks for this correction.  I was confusing arbitrary judgments and {|-} judgments, which was the point of your question.  This confusion also was part of my comment about the query and map tactics.  The query tactic works on arbitrary judgments so it is needed.  The map predicate I proposed only works on {|-} judgments and isn't needed since one can just use inst instead.

 

The main theorem in examples/misc/copy proves one direction (the `copy_align` theorem) this way with an `inst`, and the other direction (the `copy2_align` theorem) using an induction. Part of my question was about how general the induction technique is: it doesn't seem to depend on much, even if it is not universally valid. And I'm interested in hearing what others have to say about the second part of my question concerning "completeness".

I should add that this kind of theorem comes up all the time when proving the correctness of an elaboration that simulates some constructors (like `let`) in terms of others (like 'lam` and `ap`), when f is usually the same as g and represents the simulation relation. The terms in the first argument of f are from the whole system and the terms from the second argument are from the subset. In the rules defining f, you have the choice when descending under binders between, e.g.,

f (lam E) (lam E') :- pi x\ f x x => f (E x) (E' x).

and

f (lam E) (lam E') :- pi x\ pi y\ f x y => f (E x) (E' y).

The second choice makes it easy to show that the relation is preserved under substitution, since you can instantiate x and y independently, but has the disadvantage that, during lifting, instances of x will appear in the E' terms, and you have to prove a strengthening lemma to show that these occurrences can't actually happen (i.e., that, more or less, the x's only appear in the first argument and the y's only appear in the second). The first choice eliminates this problem, but then you can't handle independent substitutions, unless you prove a lemma like the one I was originally asking about.

I think that there is something deep here that we haven't described well enough yet.  One reason for saying this is that this seems closely related to the definition and meta-theory of logical relations (a semantic technique that is often employed for the kind of simulation proofs you are considering).  The definition of lifting a logical relation to higher types makes use of clauses such as

rel (lam E) (lam E') :- pi x\ pi y\ rel x y => rel (E x) (E' y).

for constructors of second-order type (such as lam).   An important result about logic relations is

|- forall x, rel x x

 

As a side question, if anyone has some successful experience navigating these issues to prove elaborations or simulations between systems, I'd be interested in seeing how you did it.

I've done some simulation proofs in the context of the pi-calculus but those proofs were more "first-order" and not of the kind you are looking at.  I also would like to hear from others on this topic.

[Todd Wilson]

These issues have come up again for me in the latest development I am working on, and I'm fighting again with the implications of defining binary relations by introducing two variables vs. one when descending under object-level binders. Has anyone thought more about this and have any answers to the questions I raised in this thread from Fall 2021? (See below for that initial post and the rest of the thread for some more information.)

[Dale Miller]

Dear Todd,

Unfortunately, I have not thought about this issue of quantification for defining binary predicates, even though I agree that it's an interesting problem.  I haven't worked much on Abella and metatheory in the past few years.

One thing that will eventually be useful for me will be seeing examples of these issues and how people have addressed them.  I hope to eventually see your approach to specific examples of specifying binary relations.

Best, Dale