Changes between Version 91 and Version 92 of TypeFunctionsSolving


Ignore:
Timestamp:
Sep 14, 2008 5:15:39 AM (7 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.