On Representability of Multiple-Valued Functions by Linear Lambda Terms Typed with Second-order Polymorphic Type System
This work addresses a foundational problem in theoretical computer science for researchers in type theory and functional programming, but it appears incremental as it builds on existing concepts of lambda calculus and type systems.
The paper tackles the problem of representing multiple-valued functions using linear lambda terms in a second-order polymorphic type system, achieving this through two distinct styles: a circuit style mimicking combinational circuits and an inductive style following a traditional mathematical approach, with optimizations and a case study demonstrating potential applications.
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.