• Yue Li – Productive Corecursion in Logic Programming (10 May, 2017)

    by  • September 8, 2017 • DSG Research Seminars: Logic and Programming Languages

    Logic Programming is a Turing complete language. As a consequence, designing algorithms that decide termination and non-termination of programs or decide inductive/coinductive soundness of formulae is a challenging task. For example, the existing state-of-the-art algorithms can only semi-decide coinductive soundness of queries in logic programming for regular formulae. Another, less famous, but equally fundamental and important undecidable property is productivity. If a derivation is infinite and coinductively sound, we may ask whether the computed answer it determines actually computes an infinite formula. If it does, the infinite computation is productive. This intuition was first expressed under the name of computations at infinity in the 80s. In modern days of the Internet and stream processing, its importance lies in connection to infinite data structure processing.

    Recently, an algorithm was presented that semi-decides a weaker property — of productivity of logic programs. A logic program is productive if it can give rise to productive derivations. In this talk I will strengthen these recent results. I will propose a method that semi-decides productivity of individual derivations for regular formulae. Thus I will give an algorithmic counterpart to the notion of productivity of derivations in logic programming. This is the first algorithmic solution to the problem since it was raised more than 30 years ago. I will also present an implementation of this algorithm.

    About