The vectorial -calculus

DOI10.1016/J.IC.2017.04.001zbMATH Open1370.68045arXiv1308.1138OpenAlexW21537352MaRDI QIDQ529049FDOQ529049

Authors: Pablo Arrighi, Alejandro Díaz-Caro, Benoît Valiron 

Publication date: 18 May 2017

Published in: Information and Computation (Search for Journal in Brave)

Abstract: We describe a type system for the linear-algebraic $lambda$-calculus. The type system accounts for the linear-algebraic aspects of this extension of $lambda$-calculus: it is able to statically describe the linear combinations of terms that will be obtained when reducing the programs. This gives rise to an original type theory where types, in the same way as terms, can be superposed into linear combinations. We prove that the resulting typed $lambda$-calculus is strongly normalising and features weak subject reduction. Finally, we show how to naturally encode matrices and vectors in this typed calculus.

Full work available at URL: https://arxiv.org/abs/1308.1138

Recommendations

• A type system for the vectorial aspect of the linear-algebraic lambda-calculus
• scientific article
• A System F accounting for scalars
• Scalar System F for linear-algebraic \(\lambda\)-calculus: towards a quantum physical logic
• A typed, algebraic, computational lambda-calculus

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Cites Work

• Title not available (Why is that?)
• Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer
• Nondeterministic extensions of untyped \(\lambda\)-calculus
• Probabilistic operational semantics for the lambda calculus
• Title not available (Why is that?)
• Non-idempotent intersection types and strong normalisation
• Bounding normalization time through intersection types
• The differential lambda-calculus
• A Lambda Calculus for Quantum Computation
• Title not available (Why is that?)
• Lambda-calculi for (strict) parallel functions
• A relational semantics for parallelism and non-determinism in a functional setting
• Adding algebraic rewriting to the untyped lambda calculus
• Intersection and union types: Syntax and semantics
• Title not available (Why is that?)
• A computational definition of the notion of vectorial space
• A System F accounting for scalars
• Linearity in the non-deterministic call-by-value setting
• Call-by-value, call-by-name and the vectorial behaviour of the algebraic \(\lambda \)-calculus
• Title not available (Why is that?)
• Linearity, non-determinism and solvability
• Probabilistic  -calculus and Quantitative Program Analysis
• Quantitative types for the linear substitution calculus
• Call-by-value non-determinism in a linear logic type discipline
• A Polymorphic Type System for the Lambda-Calculus with Constructors
• The algebraic lambda calculus
• The λ-calculus with constructors: Syntax, confluence and separation
• Completion of a Set of Rules Modulo a Set of Equations
• Title not available (Why is that?)
• Title not available (Why is that?)
• Intersection types from a proof-theoretic perspective
• A type system for the vectorial aspect of the linear-algebraic lambda-calculus
• The probability of non-confluent systems
• Typing Quantum Superpositions and Measurement
• Confluence via strong normalisation in an algebraic \(\lambda\)-calculus with rewriting

Cited In (18)

• Finite vector spaces as model of simply-typed lambda-calculi
• Title not available (Why is that?)
• A concrete model for a typed linear algebraic lambda calculus
• Title not available (Why is that?)
• Linear-algebraic λ-calculus: higher-order, encodings, and confluence.
• A Lambda Calculus for Density Matrices with Classical and Probabilistic Controls
• Extensional proofs in a propositional logic modulo isomorphisms
• A type system for the vectorial aspect of the linear-algebraic lambda-calculus
• Matrices as arrows! A biproduct approach to typed linear algebra
• A concrete categorical semantics of lambda-\(\mathcal{S}\)
• The differential \(\lambda \mu\)-calculus
• A System F accounting for scalars
• Scalar System F for linear-algebraic \(\lambda\)-calculus: towards a quantum physical logic
• A quick overview on the quantum control approach to the lambda calculus
• A typed, algebraic, computational lambda-calculus
• Typing Quantum Superpositions and Measurement
• A classical linear \(\lambda\)-calculus
• Semantics of a typed algebraic lambda-calculus

Uses Software

• Automath

This page was built for publication: The vectorial \(\lambda\)-calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q529049)