Changes between Version 10 and Version 11 of TypeFunctionsSolving


Ignore:
Timestamp:
Jul 23, 2008 6:44:21 AM (6 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSolving

    v10 v11  
    2323 * Perform Rule Triv as part of normalisation. 
    2424 * Whenever an equality of Form (2) or (3) would be recursive, the program can be rejected on the basis of a failed occurs check.  (Immediate rejection is always justified, as right-hand sides do not contain synonym familles; hence, any recursive occurrences of a left-hand side imply that the equality is unsatisfiable.) 
    25  * Use flexible tyvars for flattening of locals, too. 
     25 * Use flexible tyvars for flattening of locals, too.  (We have flexibles in locals anyway and don't use (Unify) on locals, so the flexibles shouldn't cause any harm, but the elimination of skolems is much easier for flexibles - we just instantiate them.) 
     26 * Do we need to record a skolem elimination substitution for skolems introduced during flattening for wanteds, too? 
    2627 
    2728 
     
    7980}}} 
    8081 
    81 Derivation with modified rules: 
     82Same, but de-prioritise (Local) rewriting with equalities of Forms (2) & (3): 
     83{{{ 
     84[F v] ~ v  ||-  [F v] ~ v 
     85==> normalise 
     86v ~ [a], F v ~ a  ||-  v ~ [x], F v ~ x 
     87a := F v 
     88==> (Local) with F v 
     89v ~ [a], F v ~ a  ||-  v ~ [x], x ~ a 
     90==> (Unify) 
     91v ~ [a], F v ~ a  ||-  v ~ [a] 
     92==> (Local) with v 
     93v ~ [a], F [a] ~ a ||- [a] ~ [a] 
     94==> normalise 
     95v ~ [a], F [a] ~ a ||- 
     96QED 
     97}}} 
     98 
     99Problem is that we still fail to terminate for unsatisfiable queries: 
     100{{{ 
     101[F v] ~ v  ||-  [G v] ~ v 
     102==> normalise 
     103v ~ [a], F v ~ a  ||-  v ~ [x], G v ~ x 
     104a := F v 
     105==> (Local) with v 
     106F [a] ~ a  ||-  [a] ~ [x], G [a] ~ x 
     107==> normalise 
     108F [a] ~ a  ||-  x ~ a, G [a] ~ x 
     109==> (Unify) 
     110F [a] ~ a  ||-  G [a] ~ a 
     111==> (Top) 
     112[F a] ~ a  ||-  G [a] ~ a 
     113==> normalise 
     114a ~ [b], F a ~ b  ||-  G [a] ~ a 
     115b := F a 
     116..and so on.. 
     117}}} 
     118 
     119Is the algorithm semi-decidable? 
     120 
     121Derivation when normalisation of locals uses flexible tyvars, too - simulates the effect of (!SkolemOccurs): 
    82122{{{ 
    83123[F v] ~ v  ||-  [F v] ~ v 
     
    100140}}} 
    101141 
     142Problem is that with rank-n signatures, we do want to use (Local) with flexible tyvars.