FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Homogeneity without Loss of Generality

Author: Paweł Parys

Paper Information

Title:Homogeneity without Loss of Generality
Authors:Paweł Parys
Proceedings:FSCD Presented Papers
Editor: Helene Kirchner
Keywords:higher-order recursion schemes, lambda-calculus, homogeneous types, safe schemes
Abstract:

ABSTRACT. We consider higher-order recursion schemes as generators of infinite trees. A sort (simple type) is called homogeneous when all arguments of higher order are taken before any arguments of lower order. We prove that every scheme can be converted into an equivalent one (i.e, generating the same tree) that is homogeneous, that is, uses only homogeneous sorts. Then, we prove the same for safe schemes: every safe scheme can be converted into an equivalent safe homogeneous scheme. Furthermore, we compare two definition of safe schemes: the original definition of Damm, and the modern one. Finally, we prove a lemma which illustrates usefulness of the homogeneity assumption. The results are known, but we prove them in a novel way: by directly manipulating considered schemes.

Pages:15
Talk:Jul 11 09:30 (Session 60C: Lambda Calculus)
Paper: