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
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