A lambda calculus with naive substitution

AbstractAn alternative approach is proposed to the basic definitions of the lassical lambda calculus. A proof is sketched of the equivalence of the approach with the classical case. The new formulation simplifies some aspects of the syntactic theory of the lambda calculus. In particular it provides a justification for omitting in syntactic theory discussion of changes of bound variable.

Download Full-text

An alternative approach to study irrotational periodic gravity water waves

Zeitschrift für angewandte Mathematik und Physik ◽

10.1007/s00033-021-01578-8 ◽

2021 ◽

Vol 72 (4) ◽

Author(s):

Biswajit Basu ◽

Calin I. Martin

Keyword(s):

Free Surface ◽

Water Waves ◽

Water Wave ◽

Wave Problem ◽

Water Wave Problem ◽

Stagnation Points ◽

Alternative Approach ◽

New Formulation ◽

Bounded Below ◽

Surface Dynamic

AbstractWe are concerned here with an analysis of the nonlinear irrotational gravity water wave problem with a free surface over a water flow bounded below by a flat bed. We employ a new formulation involving an expression (called flow force) which contains pressure terms, thus having the potential to handle intricate surface dynamic boundary conditions. The proposed formulation neither requires the graph assumption of the free surface nor does require the absence of stagnation points. By way of this alternative approach we prove the existence of a local curve of solutions to the water wave problem with fixed flow force and more relaxed assumptions.

Download Full-text

A Complete, Co-Inductive Syntactic Theory of Sequential Control and State

BRICS Report Series ◽

10.7146/brics.v14i4.21927 ◽

2007 ◽

Vol 14 (4) ◽

Cited By ~ 2

Author(s):

Kristian Støvring ◽

Søren B. Lassen

Keyword(s):

Normal Form ◽

Lambda Calculus ◽

Higher Order ◽

Syntactic Theory ◽

Sequential Control ◽

Contextual Equivalence

We present a new co-inductive syntactic theory, eager normal form bisimilarity, for the untyped call-by-value lambda calculus extended with continuations and mutable references.<br /> <br />We demonstrate that the associated bisimulation proof principle is easy to use and that it is a powerful tool for proving equivalences between recursive imperative higher-order programs.<br /> <br />The theory is modular in the sense that eager normal form bisimilarity for each of the calculi extended with continuations and/or mutable references is a fully abstract extension of eager normal form bisimilarity for its sub-calculi. For each calculus, we prove that eager normal form bisimilarity is a congruence and is sound with respect to contextual equivalence. Furthermore, for the calculus with both continuations and mutable references, we show that eager normal form bisimilarity is complete: it coincides with contextual equivalence.

Download Full-text

A Study of Syntactic and Semantic Artifacts and its Application to Lambda Definability, Strong Normalization, and Weak Normalization in the Presence of...

BRICS Report Series ◽

10.7146/brics.v15i3.21938 ◽

2008 ◽

Vol 15 (3) ◽

Cited By ~ 9

Author(s):

Johan Munk

Keyword(s):

Lambda Calculus ◽

Expressive Power ◽

Strong Normalization ◽

Syntactic Theory ◽

Abstract Machines ◽

Value Representation

Church's lambda-calculus underlies the syntax (i.e., the form) and the semantics (i.e., the meaning) of functional programs. This thesis is dedicated to studying man-made constructs (i.e., artifacts) in the lambda calculus. For example, one puts the expressive power of the lambda calculus to the test in the area of lambda definability. In this area, we present a course-of-value representation bridging Church numerals and Scott numerals. We then turn to weak and strong normalization using Danvy et al.'s syntactic and functional correspondences. We give a new account of Felleisen and Hieb's syntactic theory of state, and of abstract machines for strong normalization due to Curien, Crégut, Lescanne, and Kluge.

Download Full-text

On One-Pass CPS Transformations

BRICS Report Series ◽

10.7146/brics.v9i3.21722 ◽

2002 ◽

Vol 9 (3) ◽

Cited By ~ 1

Author(s):

Olivier Danvy ◽

Lasse R. Nielsen

Keyword(s):

Lambda Calculus ◽

Higher Order ◽

The Other ◽

Post Processing ◽

Syntactic Theory ◽

Transformation Time ◽

Phd Thesis ◽

Church Encoding ◽

Implementation Technique ◽

Syntactic Theories

We bridge two distinct approaches to one-pass CPS transformations, i.e., CPS transformations that reduce administrative redexes at transformation time instead of in a post-processing phase. One approach is compositional and higher-order, and is due to Appel, Danvy and Filinski, and Wand, building on Plotkin's seminal work. The other is non-compositional and based on a syntactic theory of the lambda-calculus, and is due to Sabry and Felleisen. To relate the two approaches, we use Church encoding, Reynolds's defunctionalization, and an implementation technique for syntactic theories, refocusing, developed in the second author's PhD thesis.

Download Full-text