Re: A question about structural congruence

[Joachim Parrow <joachim@xxxxxxxxx>]

I have not seen anything like it. The problem may be tougher than it first
appears. But I don't understand the emphasis on n # m. Would it not be simpler
to consider, by alpha-conversion,

if (nu n) P = (nu n)Q then either P = Q or
                             exists P',Q': P = (nu n)P', Q = (nu n)Q', P'=Q'

A proof  idea might be to work by induction on the length of the inference of
(nu n)P = (nu n)Q. The problem is to find a good induction hypothesis. The
main culprit is scope extension - if the last step in that inference was scope
extension we are left with a shorter inference of something like (nu n)P = Q1|
(nu n)Q2, so we need the IH to apply also to that sort of equation.

A more ambitious attack would be to find a good model for structural
congruence. I believe that is still open despite the ten years (someone here
wanted open problems...)

Joachim

  
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The "models for mobility" mailing list     mailto:moca@xxxxxxxxxxxxxxx
 http://www-sop.inria.fr/mimosa/personnel/Davide.Sangiorgi/moca.html