The vectorial -calculus

DOI10.1016/J.IC.2017.04.001MaRDI QIDQ529049zbMATH OpenOpenAlexFDO

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)

Full work available at URL https://arxiv.org/abs/1308.1138, http://hdl.handle.net/11336/72528

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

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.

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

Cites work

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

Cited in

(18)

• Semantics of a typed algebraic lambda-calculus
• Finite vector spaces as model of simply-typed lambda-calculi
• scientific article; zbMATH DE number 7559280 (Why is no real title available?)
• A concrete model for a typed linear algebraic lambda calculus
• scientific article; zbMATH DE number 7136664 (Why is no real title available?)
• 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
• A classical linear \(\lambda\)-calculus
• Typing Quantum Superpositions and Measurement

Describes a project that uses

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)