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

2008 ◽  
Vol 15 (3) ◽  
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.

A lambda calculus with naive substitution

1979 ◽  
Vol 28 (3) ◽  
pp. 269-282 ◽  
Author(s):  
John Staples
Keyword(s):  
Lambda Calculus ◽  
Classical Case ◽  
Syntactic Theory ◽  
Alternative Approach ◽  
New Formulation

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.

scholarly journals HOPLA--A Higher-Order Process Language

2002 ◽  
Vol 9 (49) ◽  
Author(s):  
Mikkel Nygaard ◽  
Glynn Winskel
Keyword(s):  
Operational Semantics ◽  
Lambda Calculus ◽  
Expressive Power ◽  
Higher Order ◽  
Domain Theory ◽  
Order Process ◽  
Encode Process ◽  
Mobile Ambients ◽  
Computation Path ◽  
Congruence Properties

A small but powerful language for higher-order nondeterministic processes is introduced. Its roots in a linear domain theory for concurrency are sketched though for the most part it lends itself to a more operational account. The language can be viewed as an extension of the lambda calculus with a ``prefixed sum'', in which types express the form of computation path of which a process is capable. Its operational semantics, bisimulation, congruence properties and expressive power are explored; in particular, it is shown how it can directly encode process languages such as CCS, CCS with process passing, and mobile ambients with public names.

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

2007 ◽  
Vol 14 (4) ◽  
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.

Termination of rewriting in the Calculus of Constructions

2003 ◽  
Vol 13 (2) ◽  
pp. 339-414 ◽  
Author(s):  
DARIA WALUKIEWICZ-CHRZĄSZCZ
Keyword(s):  
Lambda Calculus ◽  
Term Rewriting ◽  
Higher Order ◽  
Strong Normalization ◽  
Term Rewriting System ◽  
Calculus Of Constructions ◽  
Path Ordering ◽  
Higher Order Functions ◽  
Rewriting Rules ◽  
Recursive Path

We show how to incorporate rewriting into the Calculus of Constructions and we prove that the resulting system is strongly normalizing with respect to beta and rewrite reductions. An important novelty of this paper is the possibility to define rewriting rules over dependently typed function symbols. We prove strong normalization for any term rewriting system, such that all function symbols satisfy the, so called, star dependency condition, and every rule is accepted by the Higher Order Recursive Path Ordering (which is an extension of the method created by Jouannaud and Rubio for the setting of the simply typed lambda calculus). The proof of strong normalization is done by using a typed version of reducibility candidates due to Coquand and Gallier. Our criterion is general enough to accept definitions by rewriting of many well-known higher order functions, for example dependent recursors for inductive types or proof carrying functions. This makes it a very good candidate for inclusion in a proof assistant based on the Curry-Howard isomorphism.

scholarly journals Decomposing Probabilistic Lambda-Calculi

2020 ◽  
pp. 136-156
Author(s):  
Ugo Dal Lago ◽  
Giulio Guerrieri ◽  
Willem Heijltjes
Keyword(s):  
Lambda Calculus ◽  
Strong Normalization ◽  
Reduction Strategy ◽  
Fine Grained ◽  
Probabilistic Evaluation

AbstractA notion of probabilistic lambda-calculus usually comes with a prescribed reduction strategy, typically call-by-name or call-by-value, as the calculus is non-confluent and these strategies yield different results. This is a break with one of the main advantages of lambda-calculus: confluence, which means results are independent from the choice of strategy. We present a probabilistic lambda-calculus where the probabilistic operator is decomposed into two syntactic constructs: a generator, which represents a probabilistic event; and a consumer, which acts on the term depending on a given event. The resulting calculus, the Probabilistic Event Lambda-Calculus, is confluent, and interprets the call-by-name and call-by-value strategies through different interpretations of the probabilistic operator into our generator and consumer constructs. We present two notions of reduction, one via fine-grained local rewrite steps, and one by generation and consumption of probabilistic events. Simple types for the calculus are essentially standard, and they convey strong normalization. We demonstrate how we can encode call-by-name and call-by-value probabilistic evaluation.

scholarly journals A Concrete Framework for Environment Machines

2005 ◽  
Vol 12 (15) ◽  
Author(s):  
Malgorzata Biernacka ◽  
Olivier Danvy
Keyword(s):  
Lambda Calculus ◽  
Intermediate Step ◽  
Common Belief ◽  
Normal Order ◽  
Abstract Machine ◽  
Abstract Machines ◽  
Reduction Strategies ◽  
Explicit Substitutions ◽  
One Step ◽  
The Common

We materialize the common belief that calculi with explicit substitutions provide an intermediate step between an abstract specification of substitution in the lambda-calculus and its concrete implementations. To this end, we go back to Curien's original calculus of closures (an early calculus with explicit substitutions), we extend it minimally so that it can express one-step reduction strategies, and we methodically derive a series of environment machines from the specification of two one-step reduction strategies for the lambda-calculus: normal order and applicative order. The derivation extends Danvy and Nielsen's refocusing-based construction of abstract machines with two new steps: one for coalescing two successive transitions into one, and one for unfolding a closure into a term and an environment in the resulting abstract machine. The resulting environment machines include both the idealized and the original versions of Krivine's machine, Felleisen et al.'s CEK machine, and Leroy's Zinc abstract machine.

Sign in / Sign up

Export Citation Format

Share Document