Wyniki wyszukiwania - BazTech

1

New Semantical Insights Into Call-by-Value λ-Calculus

Manzonetto Giulio, Pagani Michele, Ronchi Della Rocca Simona

Fundamenta Informaticae

|

2019

|

Vol. 170, nr 1-3

241--256

EN

Despite the fact that call-by-value λ-calculus was defined by Plotkin in 1977, we believe that its theory of program approximation is still at the beginning. A problem that is often encountered when studying its operational semantics is that, during the reduction of a λ-term, some redexes remain stuck (waiting for a value). Recently, Carraro and Guerrieri proposed to endow this calculus with permutation rules, naturally arising in the context of linear logic proof-nets, that succeed in unblocking a certain number of such redexes. In the present paper we introduce a new class of models of call-by-value λ-calculus, arising from non-idempotent intersection type systems. Beside satisfying the usual properties as soundness and adequacy, these models validate the permutation rules mentioned above as well as some reductions obtained by contracting suitable λI-redexes. Thanks to these (perhaps unexpected) features, we are able to demonstrate that every model living in this class satisfies an Approximation Theorem with respect to a refined notion of syntactic approximant. While this kind of results often require impredicative techniques like reducibility candidates, the quantitative information carried by type derivations in our system allows us to provide a combinatorial proof.

2

The quasi-relevant 3-valued logic RM3 and some of its sublogics lacking the variable-sharing property

Robles G.

Reports on Mathematical Logic

|

2016

|

Vol. 51

105--131

EN

The logic RM3 is the 3-valued extension of the logic R-Mingle (RM). RM (and so, RM3) does not have the variable- sharing property (vsp), but RM3 (and so, RM) lacks the more “offending" “paradoxes of relevance”, such as A → (B → A) or ⌐A → (A → B). Thus, RM and RM3 can be useful when “some relevance”, but not the full vsp, is needed. Sublogics of RM3 with the vsp are well known, but this is not the case with those lacking this property. The first aim of this paper is to define an ample family of sublogics of RM3 without the vsp. The second one is to provide these sublogics and RM3 itself with a general Routley- Meyer semantics, that is, the semantics devised for relevant logics in the early seventies of the past century.

3

Towards a Formal Representation of Interactive Systems

Banu-Demergian I. T., Stefanescu G.

Fundamenta Informaticae

|

2014

|

Vol. 131, nr 3-4

313--336

EN

Powerful algebraic techniques have been developed for classical sequential computation. Many of them are based on regular expressions and the associated regular algebra. For parallel and interactive computation, extensions to handle 2-dimensional patterns are often required. Finite interactive systems, a 2-dimensional version of finite automata, may be used to recognize 2-dimensional languages. In this paper we present a blueprint for getting a formal representation of parallel, interactive programs and of their semantics. It is based on a recently introduced approach for getting regular expressions for 2-dimensional patterns, particularly using words of arbitrary shapes and powerful control mechanisms on composition. We extend the previously defined class of expressions n2RE with new control features, progressively increasing the expressive power of the formalism up to a level where a procedure for generating the words accepted by finite interactive systems may be obtained. Targeted applications come from the area of modelling, specification, analysis and verification of structured interactive programs via the associated scenario semantics.

4

A proff system for dependencies for information relations

MacCaull W.

Fundamenta Informaticae

|

2000

|

Vol. 42, Nr 1

1-27

EN

Using a relational approach, we investigate the implication problem for dependencies for in-formation relations, focusing on functional dependencies, association rules and multivalued dependencies. We develop a Rasiowa/Sikorski-style relational calculus and show that the as-sociated tableaux style of reasoning gives a decidable procedure for each of the three kinds of inference problems under consideration. This work has applications to classical database the-ory and to Rough Set Theory. The techniques may be generalized to the many other data de-pendencies which have formulations via binary relations and they can be applied to other in-formation relations which arise in the study of incomplete information.