Találati lista | Tudóstér

001-es BibID:	BIBFORM110536
035-os BibID:	(WoS)000933733600001
Első szerző:	Battyányi Péter (informatikus, matematikus)
Cím:	Normalization in the simply typed lambda mu mu' rho theta epsilon-calculus / Péter Battyányi, Karim Nour
Dátum:	2023
ISSN:	0960-1295
Megjegyzések:	In this paper, in connection with the program of extending the Curry-Howard isomorphism to classical logic, we study the lambda mu-calculus of Parigot emphasizing the difference between the original version of Parigot and the version of de Groote in terms of normalization properties. In order to talk about a satisfactory representation of the integers, besides the usual beta-, mu-, and mu'-reductions, we consider the lambda mu-calculus augmented with the reduction rules rho,theta and epsilon. We show that we need all of these rules for this purpose. Then we prove that, with the syntax of Parigot, the calculus enjoys the strong normalization property even when we add the rules rho,theta, and epsilon, while the lambda mu-calculus presented with the more flexible de Groote-style syntax, in contrast, has only the weak normalization property. In particular, we present a normalization algorithm for the beta mu mu 0 theta epsilon-reduction in the de Groote-style calculus.
Tárgyszavak:	Természettudományok Matematika- és számítástudományok idegen nyelvű folyóiratközlemény külföldi lapban folyóiratcikk lambda mu-calculus classical logic strong normalization weak normalization normalization algorithm
Megjelenés:	Mathematical Structures In Computer Science. - 32 : 8 (2023), p. 1066-1098. -
További szerzők:	Karim, Nour
Internet cím:	Szerző által megadott URL DOI Intézményi repozitóriumban (DEA) tárolt változat
Borító:
Saját polcon: