Wyniki wyszukiwania - Biblioteka Nauki

1

Very Simple Chaitin Machines for Concrete AIT

100%

Stay M.

Fundamenta Informaticae

|

2005

|

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

2

A Tutorial Implementation of a Dependently Typed Lambda Calculus

100%

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

Fundamenta Informaticae

|

2010

|

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

3

Marginalia to a theorem of Jacopini

100%

Statman R.

Fundamenta Informaticae

|

2001

|

tom Vol. 45, nr 1,2

117-121

EN

In 1975, G. Jacopini proved the existence of an easy term, i.e., a term which can be consistently (with beta conversion) identified with any other term. In 1980, A. Visser generalized Jacopini's result to R.E. theories; namely, easy terms for consistent (with beta conversion) R.E. theories exist. Of course, no such generalization for non-R.E. theories exists. For example, it is easy to see that there is no easy term for Barendregt's theory H. In this note we shall generalize Jacopini's result to non-R.E. theories as follows. Say that an equation M = N is easy if for any consistent (with beta conversion) extension T we have that T Č{ M = N} is consistent. We shall prove that easy equations exist.

4

Object Complexity

100%

Szczypka E.

Schedae Informaticae

|

2004

|

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

5

Decidability of Several Concepts of Finiteness for Simple Types

80%

Santo J. E. , Matthes R. , Pinto L.

Fundamenta Informaticae

|

2019

|

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

6

A Behavioural Lambda Model

80%

Dezani-Ciangaglini M. , Ghilezan S.

Schedae Informaticae

|

2003

|

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

7

Fixed point equations inside the algebra of normal forms

80%

Böhm C.

Fundamenta Informaticae

|

1999

|

tom Vol. 37, Nr 4

329-342

EN

Solutions of the equations X=ZX and X=XZ are found and discussed for Z, X normal terms of the lambda-calculus. Obviously fixed point combinators are of no help. Solutions will be independent from any kind of gödelization or coding of data structures, they will be provided by typeless self-application. Different approaches will be shown: algebraic properties, one side invertibility and idempotency. Certain subsets of proper combinators and Church alge-bras between them will be proved to be domains consisting only of fixed points of combinators.

8

Two problems on reduction graphs in lambda calculus

80%

Intrigila B. , Laurenzi A. R.

Fundamenta Informaticae

|

2000

|

tom Vol. 44, Nr 1,2

133-144

EN

In this paper we solve two open problems in the theory of reduction graphs in lambda calculus. The first question is whether the condensed reduction graph of a lambda term is always locally finite (conjecture of M.Venturini Zilli 1984). We give a negative answer to the conjecture by providing a counterexample. The second problem is whether there is a term such that its reduction graph is composed of two reduction cycles (not loops) intersecting in just one point (problem of J.W.Klop 1980). We show that such a term cannot exist.

9

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

80%

Lachowski Ł.

Reports on Mathematical Logic

|

2018

|

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

10

An outline of type-theoretical approaches to lexical semantics

80%

Cooper R. , Retoré C.

Journal of Language Modelling

|

2017

|

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

11

Church–Rosser Made Easy

80%

Kozen D.

Fundamenta Informaticae

|

2010

|

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

12

Solution to the Range Problem for Combinatory Logic

80%

Intrigila B. , Statman R.

Fundamenta Informaticae

|

2011

|

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

13

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

80%

David R. , Nour K.

Fundamenta Informaticae

|

2007

|

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

14

An axiomatic system of parametricity

80%

Takeuti I.

Fundamenta Informaticae

|

1998

|

tom Vol. 33, nr 4

397-432

EN

Plotkin and Abadi have proposed a syntactic system for parametricity based on a second order predicate logic. This paper shows three theorems about that system. The first is consistency of the system, which is proved by the method of relativization. The second is that polyadic parametricities of recursive types are equivalent to each other. The third is that the theory of parametricity for recursive types is self-realizable. As a corollary of the third theorem, the theory of parametricity for recursive types satisfies the term extraction property.

15

Reducibility Proofs in the λ-Calculus

80%

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

Fundamenta Informaticae

|

2012

|

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

16

Intersection Types from a Proof-theoretic Perspective

80%

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

Fundamenta Informaticae

|

2012

|

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

17

Nominal Unification and Matching of Higher Order Expressions with Recursive Let

70%

Schmidt-Schauß M. , Kutsia T. , Levy J. , Villaret M. , Kutz Y.

Fundamenta Informaticae

|

2022

|

tom 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

18

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

70%

Manzonetto G. , Pagani M. , Ronchi Della Rocca S.

Fundamenta Informaticae

|

2019

|

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

19

Polyadic algebras over nonclassical logics

70%

Pigozzi D. , Salibra A.

Banach Center Publications

|

1993

|

tom 28

|

nr 1

51-66

EN

The polyadic algebras that arise from the algebraization of the first-order extensions of a SIC are characterized and a representation theorem is proved. Standard implicational calculi (SIC)'s were considered by H. Rasiowa [19] and include classical and intuitionistic logic and their various weakenings and fragments, the many-valued logics of Post and Łukasiewicz, modal logics that admit the rule of necessitation, BCK logic, etc.

20

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

70%

Biasi C. , Aschieri F.

Fundamenta Informaticae

|

2008

|

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