Related papers: On reduction and normalization in the computationa…
Any set of truth-functional connectives has sequent calculus rules that can be generated systematically from the truth tables of the connectives. Such a sequent calculus gives rise to a multi-conclusion natural deduction system and to a…
Linear head reduction is a key tool for the analysis of reduction machines for lambda-calculus and for game semantics. Its definition requires a notion of redex at a distance named primary redex in the literature. Nevertheless, a clear and…
We introduce the structural resource lambda-calculus, a new formalism in which strongly normalizing terms of the lambda-calculus can naturally be represented, and at the same time any type derivation can be internally rewritten to its…
The linear-algebraic lambda-calculus and the algebraic lambda-calculus are untyped lambda-calculi extended with arbitrary linear combinations of terms. The former presents the axioms of linear algebra in the form of a rewrite system, while…
We introduce and study several notions of computability-theoretic reducibility between subsets of $\omega$ that are "robust" in the sense that if only partial information is available about the oracle, then partial information can be…
The regularization of a new problem, namely the three-body problem, using 'similar' coordinate system is proposed. For this purpose we use the relation of 'similarity', which has been introduced as an equivalence relation in a previous…
Toda's Theorem is a fundamental result in computational complexity theory, whose proof relies on a reduction from a QBF problem with a constant number of quantifiers to a model counting problem. While this reduction, henceforth called…
We observe that normalization by evaluation for simply-typed lambda-calculus with weak coproducts can be carried out in a weak bi-cartesian closed category of presheaves equipped with a monad that allows us to perform case distinction on…
We present a system to translate natural language sentences to formulas in a formal or a knowledge representation language. Our system uses two inverse lambda-calculus operators and using them can take as input the semantic representation…
The different orthogonal relationships that exists in the Lowdin orthogonalizations is presented. Other orthogonalization techniques such as polar decomposition (PD), principal component analysis (PCA) and reduced singular value…
The symmetric $\lambda \mu$-calculus is the $\lambda \mu$-calculus introduced by Parigot in which the reduction rule $\m'$, which is the symmetric of $\mu$, is added. We give arithmetical proofs of some strong normalization results for this…
We examine the reduction process of a system of second-order ordinary differential equations which is invariant under a Lie group action. With the aid of connection theory, we explain why the associated vector field decomposes in three…
Methods for the reduction of the complexity of computational problems are presented, as well as their connections to renormalization, scaling, and irreversible statistical mechanics. Several statistically stationary cases are analyzed; for…
For those of us who generally live in the world of syntax, semantic proof techniques such as reducibility, realizability or logical relations seem somewhat magical despite -- or perhaps due to -- their seemingly unreasonable effectiveness.…
The resource calculus is an extension of the lambda-calculus allowing to model resource consumption. It is intrinsically non-deterministic and has two general notions of reduction - one parallel, preserving all the possible results as a…
The lambda calculus is a widely accepted computational model of higher-order functional pro- grams, yet there is not any direct and universally accepted cost model for it. As a consequence, the computational difficulty of reducing lambda…
We present a technique to study normalizing strategies when termination is asymptotic, that is, it appears as a limit, as opposite to reaching a normal form in a finite number of steps. Asymptotic termination occurs in several settings,…
This work exploits the logical foundation of session types to determine what kind of type discipline for the pi-calculus can exactly capture, and is captured by, lambda-calculus behaviours. Leveraging the proof theoretic content of the…
Factorization -- a simple form of standardization -- is concerned with reduction strategies, i.e. how a result is computed. We present a new technique for proving factorization theorems for compound rewriting systems in a modular way, which…
The confluence of untyped lambda-calculus with unconditional rewriting has already been studied in various directions. In this paper, we investigate the confluence of lambda-calculus with conditional rewriting and provide general results in…