Semantics of a Typed Algebraic Lambda-Calculus

TL;DR

This paper develops a semantic framework for a simply-typed lambda-calculus with vector space structure, exploring its relation to existing calculi and addressing challenges with fixed point operators.

Contribution

It introduces a semantic analysis for a typed algebraic lambda-calculus with vector space structure and discusses modifications to handle fixed points.

Findings

Relation with established vectorial lambda-calculi

Problems and solutions for fixed point combinators

Sketch of algebraic vectorial PCF and interpretations

Abstract

Algebraic lambda-calculi have been studied in various ways, but their semantics remain mostly untouched. In this paper we propose a semantic analysis of a general simply-typed lambda-calculus endowed with a structure of vector space. We sketch the relation with two established vectorial lambda-calculi. Then we study the problems arising from the addition of a fixed point combinator and how to modify the equational theory to solve them. We sketch an algebraic vectorial PCF and its possible denotational interpretations.