Changes between Version 6 and Version 7 of NewAxioms/Nonlinearity


Ignore:
Timestamp:
May 29, 2013 1:43:33 PM (11 months ago)
Author:
simonpj
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • NewAxioms/Nonlinearity

    v6 v7  
    2626== The Solution == 
    2727 
    28 We need to consider the two instances of {{{F}}} to be overlapping and inadmissible. There are a handful of ways to do this, but the best seems to be this: when performing the overlap check, check a version of the instance where all variables are distinct. Using such a check, the two instances for {{{F}}} above indeed conflict. 
     28We need to consider the two instances of {{{F}}} to be overlapping and inadmissible. There are a handful of ways to do this, but the best seems to be this:  
     29 * '''when performing the overlap check between two instances, check a version of the instances where all variables are distinct''' 
     30Using such a check, the two instances for {{{F}}} above indeed conflict, because we would compare `(F a b)` against `(F [c] d)`, where a,b,c,d are the fresh distinct variables. 
    2931 
    3032This can break existing code. But, a medium-intensity search did not find ''any'' uses of nonlinear (i.e. with a repeated variable) family instances in existing code, so I think we should be OK. However, a change needs to be made -- the current system is subtly broken and has been so for years.