Wyniki wyszukiwania - BazTech

1

The Duality of Classical Intersection and Union Types

Downen Paul, Ariola Zena M., Ghilezan Silvia

Fundamenta Informaticae

|

2019

|

Vol. 170, nr 1-3

39--92

EN

For a long time, intersection types have been admired for their surprising ability to complete the simply typed lambda calculus. Intersection types are an example of an implicit typing feature which can describe program behavior without manifesting itself within the syntax of a program. Dual to intersections, union types are another implicit typing feature which extends the completeness property of intersection types in the lambda calculus to full-fledged programming languages. However, the formalization of union types can easily break other desirable meta-theoretical properties of the type system. But why should unions be troublesome when their dual, intersections, are not? We look at the issues surrounding the design of type systems for both intersection and union types through the lens of duality by formalizing them within the symmetric language of the classical sequent calculus. In order to formulate type systems which have all of our properties of interest—soundness, completeness, and type safety—we also look at the impact of evaluation strategy on typing. As a result, we present two dual type systems—one for call-by-value and one for call-by-name evaluation—which have all three properties. We also consider the possibility of classical non-deterministic evaluation, for which there is a choice between two different systems depending on which properties are desired: a full type system which is complete, and a simplified type system which is sound and type safe.

2

A semantical analysis of cut-free calculi for modal logics

Takano M.

Reports on Mathematical Logic

|

2018

|

Vol. 53

43--65

EN

We analyze semantically the logical inference rules in cut-free sequent calculi for the modal logics which are obtained from the least normal logic K by adding axioms from T, 4, 5, D and B. This implies Kripke completeness, as well as the cutelimination property or the subformula property of the calculi. By slightly modifying the arguments, the finite model property of the logics also follows.

3

Paraconsistent sequential linear-time temporal logic : combining paraconsistency and sequentiality in temporal reasoning

Kamide N.

Reports on Mathematical Logic

|

2017

|

Vol. 52

3--44

EN

Inconsistency-tolerant temporal reasoning with sequential (i.e., ordered or hierarchical) information is gaining in- creasing importance in computer science applications. A logical system for representing such reasoning is thus required for ob- taining a theoretical basis for such applications. In this paper, we introduce a new logic called paraconsistent sequential linear-time temporal logic (PSLTL), which is an extension of the standard linear-time temporal logic (LTL). PSLTL can appropriately rep- resent inconsistency-tolerant temporal reasoning with sequential information. The cut-elimination, decidability, and completeness theorems for PSLTL are proved in this paper.

4

Interpolation theorems for some variants of LTL

Kamide N.

Reports on Mathematical Logic

|

2015

|

Vol. 50

3--30

EN

It is known that Craig interpolation theorem does not hold for LTL. In this paper, Craig interpolation theorems are shown for some fragments and extensions of LTL. These theorems are simply proved based on an embedding-based proof method with Gentzen-type sequent calculi. Maksimova separation theorems (Maksimova principle of variable separation) are also shown for these LTL variants.

5

Completeness and Soundness Results for χ with Intersection and Union Types

Bakel S. van

Fundamenta Informaticae

|

2012

|

Vol. 121, nr 1/4

1-41

EN

With the eye on defining a type-based semantics, this paper defines intersection and union type assignment for the sequent calculus χ, a substitution-free language that enjoys the Curry- Howard correspondence with respect to the implicative fragment of Gentzen's sequent calculus for classical logic. We investigate the minimal requirements for such a system to be complete (i.e. closed under redex expansion), and show that the non-logical nature of both intersection and union types disturbs the soundness (i.e. closed uder reduction) properties. This implies that this notion of intersection-union type assignment needs to be restricted to satisfy soundness as well, making it unsuitable to define a semantics. We will look at two (confluent) notions of reduction, called Call-by-Name and Call-by- Value, and prove soundness results for those.

6

Characterising Strongly Normalising Intuitionistic Terms

Santo J. E., Ivetić J., Likavec S.

Fundamenta Informaticae

|

2012

|

Vol. 121, nr 1/4

83-120

EN

This paper gives a characterisation, via intersection types, of the strongly normalising proof-terms of an intuitionistic sequent calculus (where LJ easily embeds). The soundness of the typing system is reduced to that of a well known typing system with intersection types for the ordinary λ-calculus. The completeness of the typing system is obtained from subject expansion at root position. Next we use our result to analyze the characterisation of strong normalisability for three classes of intuitionistic terms: ordinary λ-terms, ΛJ-terms (λ-terms with generalised application), and λx-terms (λ-terms with explicit substitution). We explain via our system why the type systems in the natural deduction format for ΛJ and λx known from the literature contain extra, exceptional rules for typing generalised application or substitution; and we show a new characterisation of the β-strongly normalising l-terms, as a corollary to a PSN-result, relating the λ-calculus and the intuitionistic sequent calculus. Finally, we obtain variants of our characterisation by restricting the set of assignable types to sub-classes of intersection types, notably strict types. In addition, the known characterisation of the b-strongly normalising l-terms in terms of assignment of strict types follows as an easy corollary of our results.

7

A Paraconsistent Linear-time Temporal Logic

Kamide N., Wansing H.

Fundamenta Informaticae

|

2011

|

Vol. 106, nr 1

1-23

EN

Inconsistency-tolerant reasoning and paraconsistent logic are of growing importance not only in Knowledge Representation, AI and other areas of Computer Science, but also in Philosophical Logic. In this paper, a new logic, paraconsistent linear-time temporal logic (PLTL), is obtained semantically from the linear-time temporal logic LTL by adding a paraconsistent negation. Some theorems for embedding PLTL into LTL are proved, and PLTL is shown to be decidable. A Gentzentype sequent calculus PLT! for PLTL is introduced, and the completeness and cut-elimination theorems for this calculus are proved. In addition, a display calculus äPLT! for PLTL is defined.

8

Foundations of Paraconsistent Resolution

Kamide N.

Fundamenta Informaticae

|

2006

|

Vol. 71, nr 4

419-441

EN

An extended first-order predicate sequent calculus PLK with two kinds of negation is introduced as a basis of a new resolution calculus PRC (paraconsistent resolution calculus) for handling the property of paraconsistency. Herbrand theorem, completeness theorem (with respect to a classical-like semantics) and cut-elimination theorem are proved for PLK. The correspondence between PLK and PRC is shown by using a faithful embedding of PLK into the sequent calculus LK for classical logic.

9

On intuitionistic proof transformations, their complexity, and application to constructive program synthesis

Egly U., Schmitt S.

Fundamenta Informaticae

|

1999

|

Vol. 39, Nr 1,2

59-83

EN

We present a translation of intuitionistic sequent proofs from a multi-succedent calculus LJmc into a single-succedent calculus LJ. The former gives a basis for automated proof search whereas the latter is better suited for proof presentation and program construction from proofs in a system for constructive program synthesis. Well-known translations from the literature have a severe drawback; they use cuts in order to establish the transformation with the undesired consequence that the resulting program term is not intuitive. We establish a transformation based on permutation of inferences and discuss the relevant properties with respect to proof complexity and program terms. As an important result we show that LJ cannot polynomially simulate LJmc (both without the cut rule), even in the propositional fragment.

10

Multi lingual sequent calculus and coherent spaces

Jung A., Kegelmann M.

Fundamenta Informaticae

|

1999

|

Vol. 37, Nr 4

369-412

EN

We study a Gentzen style sequent calculus where the formulas on the left and right of the turnstile need not necessarily come from the same logical system. Such a sequent can be seen as a consequence between different domains of reasoning. We discuss the ingredients needed to set up the logic generalized in this fashion. The usual cut rule does not make sense for sequents which connect different logical systems because it mixes formulas from antecedent and succedent. We propose a different cut rule which addresses this problem. The new cut rule can be used as a basis for composition in a suitable category of logical sys-tems. As it turns out, this category is equivalent to coherent spaces with certain relations be-tween them. Finally, cut elimination in this set-up can be employed to provide a new explanation of the domain constructions in Samson Abramsky's Domain Theory in Logical Form.