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.
翻译:我们证明,任何多值函数均可通过第二类多态类型系统类型化的线性λ项,以两种不同风格表示。第一种是电路风格,模拟开关理论中的组合电路;第二种是归纳风格,遵循更传统的数学方法。我们还讨论了针对这些表示的若干优化策略。此外,通过案例研究展示了该方法在多个领域的潜在应用。