Changes between Version 91 and Version 92 of TypeFunctionsSolving


Ignore:
Timestamp:
Sep 14, 2008 5:15:39 AM (6 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSolving

    v91 v92  
    455455My guess is that the algorithm terminates for all satisfiable queries.  If that is correct, the entailment problem that the algorithm solves would be  semi-decidable. 
    456456 
     457'''Derivation with latest (and implemented) algorithm''': 
     458{{{ 
     459Top: 
     460  forall x. F x ~ [F x] 
     461 
     462F [a] ~ a |- 
     463=(norm)=> 
     464F [a] ~ a |- 
     465=(Top)=> 
     466[F a] ~ a |- 
     467=(norm)=> 
     468a ~ [beta], F a ~ beta |- 
     469  with beta := F a 
     470=(SubtVarFam)=> 
     471a ~ [beta], F [beta] ~ beta |- 
     472...and so on... 
     473}}} 
     474The only solution seems to be to give up on completeness and throw away ''loopy equalities'' as proposed in the ICFP'08 paper.