Wyniki wyszukiwania - BazTech

1

Nominal Unification and Matching of Higher Order Expressions with Recursive Let

Schmidt-Schauß Manfred, Kutsia Temur, Levy Jordi, Villaret Mateu, Kutz Yunus

Fundamenta Informaticae

|

2022

|

Vol. 185, nr 3

247--283

EN

A sound and complete algorithm for nominal unification of higher-order expressions with a recursive let is described, and shown to run in nondeterministic polynomial time. We also explore specializations like nominal letrec-matching for expressions, for DAGs, and for garbage-free expressions and determine their complexity. We also provide a nominal unification algorithm for higher-order expressions with recursive let and atom-variables, where we show that it also runs in nondeterministic polynomial time. In addition we prove that there is a guessing strategy for nominal unification with letrec and atom-variable that is a trade-off between exponential growth and non-determinism. Nominal matching with variables representing partial letrec-environments is also shown to be in NP

2

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.

3

Decidability of Several Concepts of Finiteness for Simple Types

Santo José Espírito, Matthes Ralph, Pinto Luís

Fundamenta Informaticae

|

2019

|

Vol. 170, nr 1-3

111--138

EN

If we consider as “member” of a simple type the outcome of any successful (possibly infinite) run of bottom-up proof search that starts from the type, then several concepts of “finiteness” for simple types are possible: the finiteness of the search space, the finiteness of any member, or the finiteness of the number of finite members (in other words, the inhabitants). In this paper we show that these three concepts are instances of the same parameterized notion of finiteness, and that a single, parameterized proof shows the decidability of all of them. One instance of this result means that termination of proof search is decidable. A separate result is that emptiness is also decidable (where emptiness is absence of “members” as above, not just absence of inhabitants). This fact is an ingredient of the main decidability result, but it also has a different application, the definition of the pruned search space - the one where branches leading to failure are chopped off. We conclude with our version of König’s lemma for simple types: a simple type has an infinite member exactly when the pruned search space is infinite.

4

On the complexity of the standard translation of lambda calculus into combinatory logic

Lachowski Ł.

Reports on Mathematical Logic

|

2018

|

Vol. 53

19--42

EN

We investigate the complexity of the standard translation of lambda calculus into combinatory logic. The main result shows that the asymptotic growth rate of the size of a translated term is Θ(n3) in worst-case, where n denotes the size of the lambda term.

5

An outline of type-theoretical approaches to lexical semantics

Cooper R., Retoré C.

Journal of Language Modelling

|

2017

|

Vol. 5, No. 2

165--178

EN

We take the opportunity of the publication of some of the papers of the ESSLLI workshop TYTLES (TYpe Theory and LExical Semantics, ESSLLI 2015, Barcelona) to provide an overview of the possibilities that type theory offers to model lexical semantics, especially the type-theoretical frameworks that properly model compositional semantics.

6

A logical approach to grammar description

Clément L., Kirman J., Salvati S.

Journal of Language Modelling

|

2015

|

Vol. 3, No. 1

87--143

EN

In the tradition of Model Theoretic Syntax, we propose a logical approach to the description of grammars. We combine in one formalism several tools that are used throughout computer science for their power of abstraction: logic and lambda calculus. We propose then a high-level formalism for describing mildly context sensitive grammars and their semantic interpretation. As we rely on the correspondence between logic and finite state automata, our method combines conciseness with effectivity. We illustrate our approach with a simple linguistic model of several interleaved linguistic phenomena involving extraction. The level of abstraction provided by logic and lambda calculus allows us not only to use this linguistic model for several languages, namely English, German, and Dutch, but also for semantic interpretation.

7

Reducibility Proofs in the λ-Calculus

Kamareddine F., Rahli V., Wells J. B.

Fundamenta Informaticae

|

2012

|

Vol. 121, nr 1/4

121-152

EN

Reducibility, despite being quite mysterious and inflexible, has been used to prove a number of properties of the λ-calculus and is well known to offer general proofs which can be applied to a number of instantiations. In this paper, we look at two related but different results in λ-calculi with intersection types. 1. We show that one such result (which aims at giving reducibility proofs of Church-Rosser, standardisation and weak normalisation for the untyped λ-calculus) faces serious problems which break the reducibility method. We provide a proposal to partially repair the method. 2. We consider a second result whose purpose is to use reducibility for typed terms in order to show the Church-Rosser of &lbeta;-developments for the untyped terms (and hence the Church- Rosser of β-reduction). In this second result, strong normalisation is not needed. We extend the second result to encompass both βI- and βη-reduction rather than simply β-reduction.

8

Intersection Types from a Proof-theoretic Perspective

Pimentel E., Ronchi della Rocca S., Roversi L.

Fundamenta Informaticae

|

2012

|

Vol. 121, nr 1/4

253-274

EN

In this work we present a proof-theoretical justification for the intersection type assignment system (IT) by means of the logical system Intersection Synchronous Logic (ISL). ISL builds classes of equivalent deductions of the implicative and conjunctive fragment of the intuitionistic logic (NJ). ISL results from decomposing intuitionistic conjunction into two connectives: a synchronous conjunction, that can be used only among equivalent deductions of NJ, and an asynchronous one, that can be applied among any sets of deductions of NJ. A term decoration of ISL exists so that it matches both: the IT assignment system, when only the synchronous conjunction is used, and the simple types assignment with pairs and projections, when the asynchronous conjunction is used. Moreover, the proof of strong normalization property for ISL is a simple consequence of the same property in NJ and hence strong normalization for IT comes for free.

9

Versatility of 'Continuations' in Discourse Semantics

Dinu A.

Fundamenta Informaticae

|

2011

|

Vol. 112, nr 4

263-280

EN

We show in this paper how the computer science concept of ’continuations’, togetherwith categorial grammars and a type shiftingmechanism, is able to account for a wide range of natural language semantic phenomena, such as hierarchical discourse structure, ellipses, accommodation and free-focus and bound-focus anaphora. The merit of continuations in the dynamic semantics framework is that they abstract away from assignment functions that are essential to the formulations of Dynamic Intensional Logic, DynamicMontague Grammar, Dynamic Predicate Logic and Discourse Representation Theory, Thus, continuation style semantic do not pose problems such as the destructive assignment problem in Dynamic Predicate Logic or the variable clash problem in Discourse Representation Theory. We argue that continuations are a versatile and powerful tool, particularly well suited to manipulate scope and long distance dependencies, phenomena that abound in natural language semantics.

10

Solution to the Range Problem for Combinatory Logic

Intrigila B., Statman R.

Fundamenta Informaticae

|

2011

|

Vol. 111, nr 2

203-222

EN

The lambda-theory H is obtained from beta-conversion by identifying all closed unsolvable terms (or, equivalently, termswithout head normal form). The range problemfor the theoryHasks whether a closed term has always (up to equality in H) either an infinite range or a singleton range (that is, it is a constant function). Here we give a solution to a natural version of this problem, giving a positive answer for the theory H restricted to Combinatory Logic. The method of proof applies also to the Lazy lambda-Calculus.

11

About Parallel and Syntactocentric Formalisms: A Perspective from the Encoding of Convergent Grammar into Abstract Categorial Grammar

Groote P., de, Pogodalla S., Pollard C.

Fundamenta Informaticae

|

2011

|

Vol. 106, nr 2-4

211-231

EN

Recent discussions of grammatical architectures have distinguished two competing approaches to the syntax-semantics interface: syntactocentrism, wherein syntactic structures are mapped or transduced to semantics (and phonology), vs. parallelism, wherein semantics (and phonology) communicates with syntax via a nondirectional (or relational) interface. This contrast arises for instance in dealing with in situ operators. The aim of this paper is threefold: first, we show how the essential content of a parallel framework, convergent grammar (CVG), can be encoded within abstract categorial grammar (ACG), a generic framework which has mainly been used, until now, to encode syntactocentric architectures. Second, using such a generic framework allows us to relate the mathematical characterization of parallelism in CVG with that of syntactocentrism in mainstream categorial grammar (CG), suggesting that the distinction between parallel and syntactocentric formalisms is superficial in nature. More generally, it shows how to provide mildly context sensitive languages (MCSL), which are a clearly defined class of languages in terms of ACG, with a relational syntax-semantics interface. Finally, while most of the studies on the generative power of ACG have been related to formal languages, we show that ACG can illuminate a linguistically motivated framework such as CVG.

12

Church–Rosser Made Easy

Kozen D.

Fundamenta Informaticae

|

2010

|

Vol. 103, nr 1-4

129-136

EN

The Church–Rosser theorem states that the λ-calculus is confluent under β-reductions. The standard proof of this result is due to Tait and Martin-Löf. In this note, we present an alternative proof based on the notion of acceptable orderings. The technique is easily modified to give confluence of the βη-calculus.

13

A Tutorial Implementation of a Dependently Typed Lambda Calculus

Löh A., McBride C., Swierstra W.

Fundamenta Informaticae

|

2010

|

Vol. 102, nr 2

177-207

EN

We present the type rules for a dependently typed core calculus together with a straightforward implementation in Haskell. We explicitly highlight the changes necessary to shift from a simply-typed lambda calculus to the dependently typed lambda calculus. We also describe how to extend our core language with data types and write several small example programs. The article is accompanied by an executable interpreter and example code that allows immediate experimentation with the system we describe.

14

A Type Driven Theory of Predication with Complex Types

Asher N.

Fundamenta Informaticae

|

2008

|

Vol. 84, nr 2

151-183

EN

This paper investigates several models of the complex type ź which is needed to analyze copredication. Previous accounts are shown to be inadequate and a new account both of ź and copredication is proposed.

15

A Term Assignment for Polarized Bi-intuitionistic Logic and its Strong Normalization

Biasi C., Aschieri F.

Fundamenta Informaticae

|

2008

|

Vol. 84, nr 2

185-205

EN

We propose a term assignment (let calculus) for Intuitionistic Logic for Pragmatics ILP_AC, a polarized sequent calculus which includes ordinary positive intuitionistic logic LJ its dual LJ and dual negations ( )^ which allow a formula to "communicate" with its dual fragment. We prove the strong normalization property for the term assignment which follows by soundly translating the let calculus into simply typed l calculus with pairings and projections. A new and simple proof of strong normalization for the latter is also provided.

16

Arithmetical Proofs of Strong Normalization Results for Symmetric [lambda]-calculi

David R., Nour K.

Fundamenta Informaticae

|

2007

|

Vol. 77, nr 4

489-510

EN

We give arithmetical proofs of the strong normalization of two symmetric l-calculi corresponding to classical logic. The first one is the [`(l)]m[(m~)]-calculus introduced by Curien & Herbelin. It is derived via the Curry-Howard correspondence from Gentzen's classical sequent calculus LK in order to have a symmetry on one side between "program" and "context" and on other side between "call-by-name" and "call-by-value". The second one is the symmetric lm-calculus. It is the lm-calculus introduced by Parigot in which the reduction rule m?, which is the symmetric of m, is added. These results were already known but the previous proofs use candidates of reducibility where the interpretation of a type is defined as the fix point of some increasing operator and thus, are highly non arithmetical.

17

Very Simple Chaitin Machines for Concrete AIT

Stay M.

Fundamenta Informaticae

|

2005

|

Vol. 68, nr 3

231--247

EN

In 1975, Chaitin introduced his celebrated Omega number, the halting probability of a universal Chaitin machine, a universal Turing machine with a prefix-free domain. The Omega number's bits are algorithmically random-there is no reason the bits should be the way they are, if we define "reason" to be a computable explanation smaller than the data itself. Since that time, only two explicit universal Chaitin machines have been proposed, both by Chaitin himself. Concrete algorithmic information theory involves the study of particular universal Turing machines, about which one can state theorems with specific numerical bounds, rather than include terms like O(1). We present several new tiny Chaitin machines (those with a prefix-free domain) suitable for the study of concrete algorithmic information theory. One of the machines, which we call Keraia, is a binary encoding of lambda calculus based on a curried lambda operator. Source code is included in the appendices. We also give an algorithm for restricting the domain of blank-endmarker machines to a prefix-free domain over an alphabet that does not include the endmarker; this allows one to take many universal Turing machines and construct universal Chaitin machines from them.

18

Object Complexity

Szczypka E.

Schedae Informaticae

|

2004

|

Vol. 13

165-177

EN

The publications are sources concerning the complexity of algorithms in respect of the complexity of input data are rather scarce, even though it is quite obvious that the complexity of algorithms strongly depends on the complexity of input data. At the same time expressions like 'almost all' or 'a certain part of' are commonly used in terminology concerning probabilistic algorithms and methods. In this paper we will attempt to take a closer look at what these expressions actually mean. Therefore we will aim to develop and systematize the theory of complexity functions.

19

A Behavioural Lambda Model

Dezani-Ciangaglini M., Ghilezan S.

Schedae Informaticae

|

2003

|

Vol. 12

35-47

EN

We build a lambda model which characterizes completely (persistently) normalizing, (persistently) head normalizing, and (persistently) weak head normalizing terms. This is proved by using the finitary logical description of the model obtained by defining a suitable intersection type assignment system.

20

Nonmodularity results for lambda calculus

Salibra A.

Fundamenta Informaticae

|

2001

|

Vol. 45, nr 4

379-392

EN

The variety (equational class) of lambda abstraction algebras was introduced to algebraize the untyped lambda calculus in the same way cylindric and polyadic algebras algebraize the first-order predicate logic. In this paper we prove that the lattice of lambda theories is not modular and that the variety generated by the term algebra of a semi-sensible lambda theory is not congruence modular. Another result of the paper is that the Mal'cev condition for congruence modularity is inconsistent with the lambda theory generated by equating all the unsolvable [lambda]-terms.