Changes between Version 91 and Version 92 of TypeFunctionsSolving
 Timestamp:
 Sep 14, 2008 5:15:39 AM (8 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

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