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 -