On Representability of Multiple-Valued Functions by Linear Lambda Terms Typed with Second-order Polymorphic Type System

TL;DR

This paper demonstrates that all multiple-valued functions can be represented by linear lambda terms within a second-order polymorphic type system, using circuit and inductive styles, with potential applications shown.

Contribution

It introduces a novel method for representing multiple-valued functions with linear lambda calculus and explores two distinct representation styles.

Findings

Both circuit and inductive styles effectively represent multiple-valued functions.

Optimizations improve the efficiency of the lambda term representations.

A case study illustrates practical applications across different domains.

Abstract

We show that any multiple-valued function can be represented by a linear lambda term typed in a second-order polymorphic type system, using two distinct styles. The first is a circuit style, which mimics combinational circuits in switching theory. The second is an inductive style, which follows a more traditional mathematical approach. We also discuss several optimizations for these representations. Furthermore, we present a case study that demonstrates the potential applications of our approach across various domains.