Wyniki wyszukiwania - BazTech

1

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.

2

Platek spaces

Ivanov L.

Fundamenta Informaticae

|

2000

|

Vol. 44, Nr 1,2

145-181

EN

The aim of this work is to axiomatize and enhance the recursion theory on monotonic hierarchies of operative spaces developed. This is to be accomplished by employing a special new variety of operative spaces called Platek spaces. The original structure studied by Platek in corresponds to the particular Platek space with structural class O = w and a bottom operative space consisting of single-valued partial functions over an arbitrary domain (Example 1.1 below). We believe that Platek spaces not only redefine Platek's approach in an abstract manner, but also provide the appropriate setting for an intrinsic Generalized Recursion Theory.

3

Boldface recursion on Platek spaces

Ivanov L.

Fundamenta Informaticae

|

2000

|

Vol. 44, Nr 1,2

183-208

EN

The present work develops a boldface version of the theory of Platek spaces initiated. This is done by studying recursion on spaces with special elements which embody the so called transfer operation, Chapter 14 affording full lambda-abstraction. Transfer is characteristic of the monotonic hierarchies of operative spaces, which hierarchies form models of a typed lambda-mu-calculus. The principal result here is a boldface version of the abstract Platek First Recursion Theorem; we prove appropriate boldface Enumeration and Second Recursion Theorems as well.

4

Lambda abstraction algebras : coordinatizing models of lambda calculus

Pigozzi D., Salibra A.

Fundamenta Informaticae

|

1998

|

Vol. 33, nr 2

149-200

EN

Lambda abstraction algebras are designed to algebraize the untyped lambda calculus in the same way cylindric and polyadic algebras algebraize the first-order logic; they are intended as an alternative to combinatory algebras in this regard. Like combinatory algebras they can be defined by true identities and thus from a variety in the sense if universal algebra. One feature of lambda abstraction algebras that sts them apart from combinatory algebras is the way variables in the lambda calculus are abtracted; this provides each lambda abstraction algebra with an implicit coordinate system. Another peculiar feature in the algebraic reformulation of (b)-conversion as the definition of abstract substitution. Functional lambda abstraction algebras arise as the 'coordinatizations' of environment models or lambda models, the natural combinatory models of the lambda calculus. As in the case of cylindric and polyadic algebras, questions of the functional representation of various subclasses of lambda abstraction algebras are an important part of the theory. The main result of the paper is a stronger version of the functional representation theorem for locally finite lambda abstraction algebras, the algebraic analogue of the completeness theorem of lambda calculus. This result is used to study the connection between the combinatory models of the lambda calculus and lambda abstraction algebras. Two significant results of this kind are the existence of a strong categorical equivalence between lambda algebras and locally finite lambda abstraction algebras, and between lambda models and rich, locally finite lambda abstraction algebras.