Games, Automata and Matching

Colin Stirling

doi:10.1007/978-3-540-73595-3_1

Games, Automata and Matching

Colin Stirling

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract / Description of output

Higher-order matching is the problem given t = u where t, u are terms of simply typed λ-calculus and u is closed, is there a substitution θ such that t θ and u have the same normal form with respect to βη-equality: can t be pattern matched to u? The problem was conjectured to be decidable by Huet [4]. Loader showed that it is undecidable when β-equality is the same normal form by encoding λ-definability as matching [6].

Original language	English
Title of host publication	Automated Deduction
Subtitle of host publication	CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings
Publisher	Springer
Pages	1-2
Number of pages	2
Volume	4603
ISBN (Electronic)	978-3-540-73595-3
ISBN (Print)	978-3-540-73594-6
DOIs	https://doi.org/10.1007/978-3-540-73595-3_1
Publication status	Published - 2007

Access to Document

10.1007/978-3-540-73595-3_1

http://dx.doi.org/10.1007/978-3-540-73595-3_1

Cite this

@inproceedings{3ee1d3c40f634cf797f33e3ec904bf16,

title = "Games, Automata and Matching",

abstract = "Higher-order matching is the problem given t = u where t, u are terms of simply typed λ-calculus and u is closed, is there a substitution θ such that t θ and u have the same normal form with respect to βη-equality: can t be pattern matched to u? The problem was conjectured to be decidable by Huet [4]. Loader showed that it is undecidable when β-equality is the same normal form by encoding λ-definability as matching [6].",

author = "Colin Stirling",

year = "2007",

doi = "10.1007/978-3-540-73595-3_1",

language = "English",

isbn = "978-3-540-73594-6",

volume = "4603",

pages = "1--2",

booktitle = "Automated Deduction",

publisher = "Springer",

address = "United Kingdom",

}

TY - GEN

T1 - Games, Automata and Matching

AU - Stirling, Colin

PY - 2007

Y1 - 2007

N2 - Higher-order matching is the problem given t = u where t, u are terms of simply typed λ-calculus and u is closed, is there a substitution θ such that t θ and u have the same normal form with respect to βη-equality: can t be pattern matched to u? The problem was conjectured to be decidable by Huet [4]. Loader showed that it is undecidable when β-equality is the same normal form by encoding λ-definability as matching [6].

AB - Higher-order matching is the problem given t = u where t, u are terms of simply typed λ-calculus and u is closed, is there a substitution θ such that t θ and u have the same normal form with respect to βη-equality: can t be pattern matched to u? The problem was conjectured to be decidable by Huet [4]. Loader showed that it is undecidable when β-equality is the same normal form by encoding λ-definability as matching [6].

U2 - 10.1007/978-3-540-73595-3_1

DO - 10.1007/978-3-540-73595-3_1

M3 - Conference contribution

SN - 978-3-540-73594-6

VL - 4603

SP - 1

EP - 2

BT - Automated Deduction

PB - Springer

ER -

Games, Automata and Matching

Abstract / Description of output

Access to Document

Fingerprint

Cite this