Intuitionistic and classical natural deduction systems with the catch and the throw rules (Q1392143)

From MaRDI portal
scientific article
Language Label Description Also known as
English
Intuitionistic and classical natural deduction systems with the catch and the throw rules
scientific article

    Statements

    Intuitionistic and classical natural deduction systems with the catch and the throw rules (English)
    0 references
    0 references
    23 July 1998
    0 references
    Two natural deduction systems \(\text{NJ}_{c/t}\) and \(\text{NK}_{c/t}\) are introduced. \(\text{NJ}_{c/t}\) is an extension of the intuitionistic natural deduction system NJ with the catch and throw rules. \(\text{NK}_{c/t}\) is an extension of the classical natural deduction system NK with the catch and throw rules. These rules are motivated from catch and throw program constructs. \(\text{NJ}_{c/t}\) and \(\text{NK}_{c/t}\) are formulated in the standard way, except that (1) an assumption variable is attached to each assumption formula in a proof figure in order to capture the mechanism of variable abstraction in the interpretation rule and disjunction elimination rule, and (2) a tag variable is attached to each premise of the throw rule in order to capture the mechanism of variable abstraction in the catch rule. The main results of the paper are that \(\text{NJ}_{c/t}\) and \(\text{NK}_{c/t}\) are logically equivalent to NJ and NK, respectively. Also an interpretation of \(\text{NJ}_{c/t}\) in terms of an extension of type-free lambda calculus by the catch and throw mechanism is given. This interpretation is an extension of the Curry-Howard isomorphism between NJ proofs and lambda terms.
    0 references
    classical natural deduction system
    0 references
    intuitionistic natural deduction system
    0 references
    functional laguages
    0 references
    lambda calculus
    0 references
    logic of programs
    0 references
    recursion
    0 references
    denotational semantics
    0 references
    equational proof system
    0 references
    completeness
    0 references
    decidability
    0 references
    catch and throw
    0 references
    0 references

    Identifiers