TY - GEN

T1 - Limiting partial combinatory algebras towards infinitary lambda-calculi and classical logic

AU - Akama, Yoji

PY - 2001/1/1

Y1 - 2001/1/1

N2 - We will construct from every partial combinatory algebra (pca, for short) A a pca a-lim(A) s.t. (1) every representable numeric function φ(n) of a-lim(A) is exactly of the form limt ξ(t, n) with ξ(t, n) being a representable numeric function of A, and (2) A can be embedded into a-lim(A) which has a synchronous application operator. Here, a-lim(A) is A equipped with a limit structure in the sense that each element of a-lim(A) is the limit of a countable sequence of A-elements. We will discuss limit structures for A in terms of Barendregt’s range property. Moreover, we will repeat the construction lim(−) transfinite times to interpret infinitary λ-calculi. Finally, we will interpret affine type-free λμ-calculus by introducing another partial applicative structure which has an asynchronous application operator and allows a parallel limit operation.

AB - We will construct from every partial combinatory algebra (pca, for short) A a pca a-lim(A) s.t. (1) every representable numeric function φ(n) of a-lim(A) is exactly of the form limt ξ(t, n) with ξ(t, n) being a representable numeric function of A, and (2) A can be embedded into a-lim(A) which has a synchronous application operator. Here, a-lim(A) is A equipped with a limit structure in the sense that each element of a-lim(A) is the limit of a countable sequence of A-elements. We will discuss limit structures for A in terms of Barendregt’s range property. Moreover, we will repeat the construction lim(−) transfinite times to interpret infinitary λ-calculi. Finally, we will interpret affine type-free λμ-calculus by introducing another partial applicative structure which has an asynchronous application operator and allows a parallel limit operation.

KW - Discontinuity

KW - Infinitary lambdacalculi

KW - Limiting recursive functions

KW - Partial combinatory algebra

KW - Realizability interpretation

KW - λμ-calculus

UR - http://www.scopus.com/inward/record.url?scp=23044529965&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=23044529965&partnerID=8YFLogxK

M3 - Conference contribution

AN - SCOPUS:23044529965

SN - 3540425543

SN - 9783540425540

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 399

EP - 414

BT - Computer Science Logic

A2 - Fribourg, Laurent

PB - Springer-Verlag

T2 - 15th International Workshop on Computer Science Logic, CSL 2001 and 10th Annual Conference of the European Association for Computer Science Logic, EACSL 2001

Y2 - 10 September 2001 through 13 September 2001

ER -