Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A concrete model for a typed linear algebraic lambda calculus

Alejandro Díaz-Caro, Octavio Malherbe

TL;DR

An adequate, concrete, categorical-based model for Lambda, which is a typed version of a linear-algebraic lambda calculus, extended with measurements, that considers S as the composition of two functors in an adjunction relation between the category of sets and the categories of vector spaces.

Abstract

We give an adequate, concrete, categorical-based model for Lambda-S, which is a typed version of a linear-algebraic lambda calculus, extended with measurements. Lambda-S is an extension to first-order lambda calculus unifying two approaches of non-cloning in quantum lambda-calculi: to forbid duplication of variables, and to consider all lambda-terms as algebraic linear functions. The type system of Lambda-S have a superposition constructor S such that a type A is considered as the base of a vector space while SA is its span. Our model considers S as the composition of two functors in an adjunction relation between the category of sets and the category of vector spaces over C. The right adjoint is a forgetful functor U, which is hidden in the language, and plays a central role in the computational reasoning.

A concrete model for a typed linear algebraic lambda calculus

TL;DR

An adequate, concrete, categorical-based model for Lambda, which is a typed version of a linear-algebraic lambda calculus, extended with measurements, that considers S as the composition of two functors in an adjunction relation between the category of sets and the categories of vector spaces.

Abstract

We give an adequate, concrete, categorical-based model for Lambda-S, which is a typed version of a linear-algebraic lambda calculus, extended with measurements. Lambda-S is an extension to first-order lambda calculus unifying two approaches of non-cloning in quantum lambda-calculi: to forbid duplication of variables, and to consider all lambda-terms as algebraic linear functions. The type system of Lambda-S have a superposition constructor S such that a type A is considered as the base of a vector space while SA is its span. Our model considers S as the composition of two functors in an adjunction relation between the category of sets and the category of vector spaces over C. The right adjoint is a forgetful functor U, which is hidden in the language, and plays a central role in the computational reasoning.

Paper Structure

This paper contains 11 sections, 12 theorems, 37 equations, 10 figures.

Table of Contents

  1. Introduction
  2. The calculus Lambda-S
  3. Denotational semantics
  4. Categorical constructions
  5. Interpretation
  6. Soundness and Adequacy
  7. Soundness
  8. Computational adequacy
  9. Adequacy
  10. Conclusion
  11. Detailed proofs

Key Result

Theorem 2.7

Lineal, an untyped fragment of Lambda-$\mathcal{S}$, is confluent. ∎

Figures (10)

  • Figure 1: Syntax of types and terms of Lambda-$\mathcal{S}$.
  • Figure 2: Typing relation
  • Figure 3: Beta rules
  • Figure 4: Linear distribution rules
  • Figure 5: Rules of the conditional construction
  • ...and 5 more figures

Theorems & Definitions (52)

  • Example 2.1
  • Example 2.2
  • Example 2.3
  • Example 2.4
  • Example 2.5
  • Example 2.6
  • Theorem 2.7: Confluence of Lineal, ArrighiDowekLMCS17
  • Theorem 2.8: Subject reduction on closed terms, DiazcaroDowekRinaldiBIO19
  • Theorem 2.9: Strong normalization, DiazcaroDowekRinaldiBIO19
  • Theorem 2.10: Progress
  • ...and 42 more