Document

**Published in:** LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)

The lambda-calculus possesses a strong notion of extensionality, called "the omega-rule", which has been the subject of many investigations. It is a longstanding open problem whether the equivalence obtained by closing the theory of Böhm trees under the omega-rule is strictly included in Morris's original observational theory, as conjectured by Sallé in the seventies. In a recent work, Breuvart et al. have shown that Morris's theory satisfies the omega-rule. In this paper we demonstrate that the two aforementioned theories actually coincide, thus disproving Sallé's conjecture.

Benedetto Intrigila, Giulio Manzonetto, and Andrew Polonsky. Refutation of Sallé's Longstanding Conjecture. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 20:1-20:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{intrigila_et_al:LIPIcs.FSCD.2017.20, author = {Intrigila, Benedetto and Manzonetto, Giulio and Polonsky, Andrew}, title = {{Refutation of Sall\'{e}'s Longstanding Conjecture}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {20:1--20:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.20}, URN = {urn:nbn:de:0030-drops-77236}, doi = {10.4230/LIPIcs.FSCD.2017.20}, annote = {Keywords: lambda calculus, observational equivalence, B\"{o}hm trees, omega-rule} }

Document

**Published in:** LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)

Working in the untyped lambda calculus, we study Morris's
lambda-theory H+. Introduced in 1968, this is the original
extensional theory of contextual equivalence. On the syntactic side,
we show that this lambda-theory validates the omega-rule, thus
settling a long-standing open problem.On the semantic side, we
provide sufficient and necessary conditions for relational graph
models to be fully abstract for H+. We show that a relational graph
model captures Morris's observational preorder exactly when it is
extensional and lambda-Konig. Intuitively, a model is lambda-Konig
when every lambda-definable tree has an infinite path which is
witnessed by some element of the model.
Both results follow from a weak separability property enjoyed by
terms differing only because of some infinite eta-expansion,
which is proved through a refined version of the Böhm-out technique.

Flavien Breuvart, Giulio Manzonetto, Andrew Polonsky, and Domenico Ruoppolo. New Results on Morris's Observational Theory: The Benefits of Separating the Inseparable. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 15:1-15:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{breuvart_et_al:LIPIcs.FSCD.2016.15, author = {Breuvart, Flavien and Manzonetto, Giulio and Polonsky, Andrew and Ruoppolo, Domenico}, title = {{New Results on Morris's Observational Theory: The Benefits of Separating the Inseparable}}, booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)}, pages = {15:1--15:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-010-1}, ISSN = {1868-8969}, year = {2016}, volume = {52}, editor = {Kesner, Delia and Pientka, Brigitte}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.15}, URN = {urn:nbn:de:0030-drops-59924}, doi = {10.4230/LIPIcs.FSCD.2016.15}, annote = {Keywords: Lambda calculus, relational models, fully abstract, B\"{o}hm-out, omega-rule} }

Document

**Published in:** LIPIcs, Volume 39, 20th International Conference on Types for Proofs and Programs (TYPES 2014)

We prove an extensionality theorem for the "type-in-type" dependent type theory with Sigma-types. We suggest that in type theory the notion of extensional equality be identified with the logical equivalence relation defined by induction on type structure.

Andrew Polonsky. Extensionality of lambda-*. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 221-250, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{polonsky:LIPIcs.TYPES.2014.221, author = {Polonsky, Andrew}, title = {{Extensionality of lambda-*}}, booktitle = {20th International Conference on Types for Proofs and Programs (TYPES 2014)}, pages = {221--250}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-88-0}, ISSN = {1868-8969}, year = {2015}, volume = {39}, editor = {Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.221}, URN = {urn:nbn:de:0030-drops-54995}, doi = {10.4230/LIPIcs.TYPES.2014.221}, annote = {Keywords: Extensionality, logical relations, type theory, lambda calculus, reflection} }

Document

**Published in:** LIPIcs, Volume 36, 26th International Conference on Rewriting Techniques and Applications (RTA 2015)

We present a coinductive framework for defining infinitary analogues of equational reasoning and rewriting in a uniform way. The setup captures rewrite sequences of arbitrary ordinal length, but it has neither the need for ordinals nor for metric convergence. This makes the framework especially suitable for formalizations in theorem provers.

Jörg Endrullis, Helle Hvid Hansen, Dimitri Hendriks, Andrew Polonsky, and Alexandra Silva. A Coinductive Framework for Infinitary Rewriting and Equational Reasoning. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 143-159, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{endrullis_et_al:LIPIcs.RTA.2015.143, author = {Endrullis, J\"{o}rg and Hansen, Helle Hvid and Hendriks, Dimitri and Polonsky, Andrew and Silva, Alexandra}, title = {{A Coinductive Framework for Infinitary Rewriting and Equational Reasoning}}, booktitle = {26th International Conference on Rewriting Techniques and Applications (RTA 2015)}, pages = {143--159}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-85-9}, ISSN = {1868-8969}, year = {2015}, volume = {36}, editor = {Fern\'{a}ndez, Maribel}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.143}, URN = {urn:nbn:de:0030-drops-51949}, doi = {10.4230/LIPIcs.RTA.2015.143}, annote = {Keywords: infinitary rewriting, coinduction} }

Document

**Published in:** LIPIcs, Volume 19, 18th International Workshop on Types for Proofs and Programs (TYPES 2011)

We provide a coinductive definition of strongly convergent reductions between infinite lambda terms. This approach avoids the notions of ordinals and metric convergence which have appeared in the earlier definitions of the concept. As an illustration, we prove the existence part of the infinitary standardization theorem. The proof is fully formalized in Coq using coinductive types. The paper concludes with a characterization of infinite lambda terms which reduce to themselves in a single beta step.

Jörg Endrullis and Andrew Polonsky. Infinitary Rewriting Coinductively. In 18th International Workshop on Types for Proofs and Programs (TYPES 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 19, pp. 16-27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{endrullis_et_al:LIPIcs.TYPES.2011.16, author = {Endrullis, J\"{o}rg and Polonsky, Andrew}, title = {{Infinitary Rewriting Coinductively}}, booktitle = {18th International Workshop on Types for Proofs and Programs (TYPES 2011)}, pages = {16--27}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-49-1}, ISSN = {1868-8969}, year = {2013}, volume = {19}, editor = {Danielsson, Nils Anders and Nordstr\"{o}m, Bengt}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2011.16}, URN = {urn:nbn:de:0030-drops-38971}, doi = {10.4230/LIPIcs.TYPES.2011.16}, annote = {Keywords: infinitary rewriting, coinduction, lambda calculus, standardization} }

Document

**Published in:** LIPIcs, Volume 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL (2011)

We study reflection in the Lambda Calculus from an axiomatic point of view. Specifically, we consider various properties that the quote operator must satisfy as a function on lambda terms. The most important of these is the existence of a definable left inverse, a so-called evaluator for the quote operator. Usually the quote operator encodes the syntax of a given term, and the evaluator proceeds by analyzing the syntax and reifying all constructors by their actual meaning in the calculus. Working in Combinatory Logic, Raymond Smullyan (1994) investigated which elements of the syntax must be accessible via the quote in order for an evaluator to exist. He asked three specific questions, to which we provide negative answers. On the positive side, we give a characterization of quotes which possess all of the desired properties, equivalently defined as being equitranslatable with a standard quote. As an application, we show that Scott's coding is not complete in this sense, but can be slightly modified to be such. This results in a minimal definition of a complete quoting for Combinatory Logic.

Andrew Polonsky. Axiomatizing the Quote. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 458-469, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{polonsky:LIPIcs.CSL.2011.458, author = {Polonsky, Andrew}, title = {{Axiomatizing the Quote}}, booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL}, pages = {458--469}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-32-3}, ISSN = {1868-8969}, year = {2011}, volume = {12}, editor = {Bezem, Marc}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.458}, URN = {urn:nbn:de:0030-drops-32493}, doi = {10.4230/LIPIcs.CSL.2011.458}, annote = {Keywords: lambda calculus, combinatory logic, quote operator, enumerator} }

X

Feedback for Dagstuhl Publishing

Feedback submitted

Please try again later or send an E-mail