A FINITE SEMANTICS OF SIMPLY-TYPED LAMBDA TERMS FOR INFINITE RUNS OF AUTOMATA

被引：26

作者：

Aehlig, Klaus ^{[1
]}

机构：

[1] Univ Coll Swansea, Dept Comp Sci, Swansea SA2 8PP, W Glam, Wales

来源：

LOGICAL METHODS IN COMPUTER SCIENCE | 2007年 / 3卷 / 03期

基金：

英国工程与自然科学研究理事会;

关键词：

Recursion Schemes; infinitary lambda calculus; automata;

D O I：

10.2168/LMCS-3(3:1)2007

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

Model checking properties are often described by means of finite automata. Any particular such automaton divides the set of infinite trees into finitely many classes, according to which state has an infinite run. Building the full type hierarchy upon this interpretation of the base type gives a finite semantics for simply-typed lambda-trees. A calculus based on this semantics is proven sound and complete. In particular, for regular infinite lambda-trees it is decidable whether a given automaton has a run or not. As regular lambda-trees are precisely recursion schemes, this decidability result holds for arbitrary recursion schemes of arbitrary level, without any syntactical restriction.

引用

页数：23

共 19 条

[1]

Aehlig K, 2005, LECT NOTES COMPUT SC, V3461, P39

[2] Continuous normalization for the lambda-calculus and Godel's T [J].

Aehlig, K ;

Joachimski, F .

ANNALS OF PURE AND APPLIED LOGIC, 2005, 133 (1-3) :39-71

[3]

Aehlig K, 2002, LECT NOTES COMPUT SC, V2471, P59

[4]

Aehlig K, 2006, LECT NOTES COMPUT SC, V4207, P104

[5]

Barendregt H, 1977, HDB MATH LOGIC, P1091

[6]

Buchholz W., 1991, Archive for Mathematical Logic, V30, P277, DOI 10.1007/BF01621472

[7]

CAUCAL D, 1996, LECT NOTES COMPUTER, V1099, P194

[8] THE MONADIC 2ND-ORDER LOGIC OF GRAPHS .9. MACHINES AND THEIR BEHAVIORS [J].

COURCELLE, B .

THEORETICAL COMPUTER SCIENCE, 1995, 151 (01) :125-162

[9]

Grigori E, 1978, Journal of Soviet Mathematics, V10, P548

[10]

Hyland JME, 2000, INFORM COMPUT, V163, P285, DOI 10.1006/inco2000.2917

← 1 2 →