Abstract:
We revisit the Vectorial λ-Calculus [3], a system that provides a way to model a vector space of terms by extending the classic terms of the λ-calculus with linear combinations of them; and by introducing a type system on top. The system can be summarized by the slogan If Γ ⊢ : T and Γ ⊢ r : R then Γ ⊢ α · t + β · r : α · T + β · R. However, the type system in Vectorial only provides a weakened version of the Subject Reduction property. We prove that our revised Vectorial λ-Calculus supports the standard version of said property as well as many others in the original system, such as Progress. We also introduce the concept of weight of types and terms, and a new property relating the weight of a term with the weight of its type.
Citación:
---------- APA ----------
Noriega, Francisco José. (2020). The vectorial Lambda calculus revisited. (Tesis de Grado. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de https://hdl.handle.net/20.500.12110/seminario_nCOM000587_Noriega
---------- CHICAGO ----------
Noriega, Francisco José. "The vectorial Lambda calculus revisited". Tesis de Grado, Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales, 2020.https://hdl.handle.net/20.500.12110/seminario_nCOM000587_Noriega
Estadísticas:
Descargas mensuales
Total de descargas desde :
https://bibliotecadigital.exactas.uba.ar/download/seminario/seminario_nCOM000587_Noriega.pdf
Distrubución geográfica
