A Coinductive Approach to Proof Search through Typed Lambda-Calculi

摘要: In reductive proof search, proofs are naturally generalized by solutions, comprising all (possibly infinite) structures generated locally correct, bottom-up application of inference rules. We propose an extension the Curry-Howard paradigm representation, from to solutions: represent solutions terms coinductive variant typed lambda-calculus that represents proofs. On this we build a new, comprehensive approach search; our case study is search in sequent calculus LJT for intuitionistic implication logic. A second, finitary representation proposed, where extended with formal greatest fixed point. latter system, fixed-point variables enjoy relaxed form binding allows detection cycles through type system. Formal sums used both representations express alternatives process, so not only individual but actually solution spaces expressed. Moreover, syntax define "decontraction" (contraction bottom-up) - operation whose theory initiate paper, and assign lambda-term each term. The main result existence equivalent any given space expressed coinductively. This underlies original builds space, posteriori analysis typically consisting applying syntax-directed procedure or function. paper illustrates potential methodology inhabitation problems simply-typed lambda-calculus, reviewing results detailed elsewhere, including new obtain extensive generalizations so-called monatomic theorem.