arXiv subjects

Ferruccio Guidi

Publications and source records attributed to Ferruccio Guidi.

3 recordsLinked to original sources

arXiv2026

An Unconventional View on Beta-Reduction in Namefree Lambda-Calculus

Terms in the lambda-calculus can be represented as planar trees decorated with symbols for abstraction and application, and having variables as leaves. In this paper, we concentrate on the branches of such trees, rather than on the trees themselves. We reformulate several well-known notions of beta-reduction in this view. In a natural manner, this reconsideration eventually leads to a new form of beta-reduction, being expanding in the sense that the reduction of term t1 to term t2 entails that the tree of t1 is a subtree of the tree of t2.

cs.LO↗

arXiv2021

A Formal System for the Universal Quantification of Schematic Variables

We advocate the use of de Bruijn's universal abstraction $λ^\infty$ for the quantification of schematic variables in the predicative setting and we present a typed $λ$-calculus featuring the quantifier $λ^\infty$ accompanied by other practically useful constructions like explicit substitutions and expected type annotations. The calculus stands just on two notions, i.e., bound rt-reduction and parametric validity, and has the expressive power of $λ\rightarrow$. Thus, while not aiming at being a logical framework by itself, it does enjoy many desired invariants of logical frameworks including confluence of reduction, strong normalization, preservation of type by reduction, decidability, correctness of types and uniqueness of types up to conversion. This calculus belongs to the $λδ$ family of formal systems, which borrow some features from the pure type systems and some from the languages of the Automath tradition, but stand outside both families. In particular, the calculus includes and evolves two earlier systems of this family. Moreover, a machine-checked specification of its theory is available.

cs.LO↗

arXiv2019

Extending the Applicability Condition in the Formal System $λδ$

The formal system $λδ$ is a typed lambda calculus derived from $Λ_\infty$, aiming to support the foundations of Mathematics that require an underlying theory of expressions (for example the Minimal Type Theory). The system is developed in the context of the Hypertextual Electronic Library of Mathematics as a machine-checked digital specification, that is not the formal counterpart of previous informal material. The first version of the calculus appeared in 2006 and proved unsatisfactory for some reasons. In this article we present a revised version of the system and we prove three relevant desired properties: the confluence of reduction, the strong normalization of an extended form of reduction, known as the "big tree" theorem, and the preservation of validity by reduction. To our knowledge, we are presenting here the first fully machine-checked proof of the "big tree" theorem for a calculus that includes $Λ_\infty$.

cs.LO↗