Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On the complexity of normalization for the planar $λ$-calculus

Anupam Das, Damiano Mazza, Lê Thành Dũng Nguyên, Noam Zeilberger

TL;DR

The paper investigates the complexity of normalization for planar untyped lambda-calculus and its relation to $\mathsf{P}$-completeness. It reevaluates a prior plan to reduce the Circuit Value Problem to planar beta-convertibility, identifying a gap caused by the non-planarity of standard copy combinators. A new approach is proposed based on bit-vector encodings and vectorial operations to simulate circuit evaluation within planar linear lambda-terms, leveraging Church-encoded tuples and carefully crafted not, and, and last operations. The work aims to establish a logspace reduction from TopCVP to planar beta-convertibility, advancing understanding of planar normalization and its computational limits.

Abstract

We sketch a tentative proof of P-completeness for the $β$-convertibility problem on untyped planar (a.k.a. ordered or non-commutative) $λ$-terms.

On the complexity of normalization for the planar $λ$-calculus

TL;DR

The paper investigates the complexity of normalization for planar untyped lambda-calculus and its relation to -completeness. It reevaluates a prior plan to reduce the Circuit Value Problem to planar beta-convertibility, identifying a gap caused by the non-planarity of standard copy combinators. A new approach is proposed based on bit-vector encodings and vectorial operations to simulate circuit evaluation within planar linear lambda-terms, leveraging Church-encoded tuples and carefully crafted not, and, and last operations. The work aims to establish a logspace reduction from TopCVP to planar beta-convertibility, advancing understanding of planar normalization and its computational limits.

Abstract

We sketch a tentative proof of P-completeness for the -convertibility problem on untyped planar (a.k.a. ordered or non-commutative) -terms.
Paper Structure (5 sections, 2 theorems, 15 equations)

This paper contains 5 sections, 2 theorems, 15 equations.

Table of Contents

  1. The Circuit Value Problem
  2. Planar booleans do not suffice
  3. A new encoding of TopCVP
  4. Representation of bit vectors
  5. Implementing vectorial operations

Key Result

Theorem 1

The following decision problem is $\mathsf{P}$-complete under logarithmic space reductions:

Theorems & Definitions (2)

  • Theorem 1: Mairson2004
  • Theorem 1.1: LimitsParallel