Higher-order strictness analysis in untyped lambda calculus

1986 ◽  
Author(s):  
Paul Hudak ◽  
Jonathan Young
Keyword(s):  
Lambda Calculus ◽  
Higher Order ◽  
Strictness Analysis

Mechanizing proofs with logical relations – Kripke-style

2018 ◽  
Vol 28 (9) ◽  
pp. 1606-1638 ◽  
Author(s):  
ANDREW CAVE ◽  
BRIGITTE PIENTKA
Keyword(s):  
Case Studies ◽  
Operational Semantics ◽  
Lambda Calculus ◽  
Equational Theory ◽  
Higher Order ◽  
Abstract Syntax ◽  
Completeness Proof ◽  
Typed Lambda Calculus ◽  
Contextual Equivalence ◽  
The Right

Proofs with logical relations play a key role to establish rich properties such as normalization or contextual equivalence. They are also challenging to mechanize. In this paper, we describe two case studies using the proof environmentBeluga: First, we explain the mechanization of the weak normalization proof for the simply typed lambda-calculus; second, we outline how to mechanize the completeness proof of algorithmic equality for simply typed lambda-terms where we reason about logically equivalent terms. The development of these proofs inBelugarelies on three key ingredients: (1) we encode lambda-terms together with their typing rules, operational semantics, algorithmic and declarative equality using higher order abstract syntax (HOAS) thereby avoiding the need to manipulate and deal with binders, renaming and substitutions, (2) we take advantage ofBeluga's support for representing derivations that depend on assumptions and first-class contexts to directly state inductive properties such as logical relations and inductive proofs, (3) we exploitBeluga's rich equational theory for simultaneous substitutions; as a consequence, users do not need to establish and subsequently use substitution properties, and proofs are not cluttered with references to them. We believe these examples demonstrate thatBelugaprovides the right level of abstractions and primitives to mechanize challenging proofs using HOAS encodings. It also may serve as a valuable benchmark for other proof environments.

An untyped higher order logic with Y combinator

2007 ◽  
Vol 72 (4) ◽  
pp. 1385-1404
Author(s):  
James H. Andrews
Keyword(s):  
Model Theory ◽  
Lambda Calculus ◽  
Higher Order ◽  
Order Logic ◽  
Proof System ◽  
Cut Elimination ◽  
Higher Order Logic ◽  
Consistent Model

AbstractWe define a higher order logic which has only a notion of sort rather than a notion of type, and which permits all terms of the untyped lambda calculus and allows the use of the Y combinator in writing recursive predicates. The consistency of the logic is maintained by a distinction between use and mention, as in Gilmore's logics. We give a consistent model theory, a proof system which is sound with respect to the model theory, and a cut-elimination proof for the proof system. We also give examples showing what formulas can and cannot be used in the logic.

scholarly journals A Complete Calculus of Monotone and Antitone Higher-Order Functions

10.29007/3n54 ◽  
2018 ◽  
Author(s):  
Thomas Icard ◽  
Lawrence Moss
Keyword(s):  
Type System ◽  
Lambda Calculus ◽  
Higher Order ◽  
Typed Lambda Calculus ◽  
Higher Order Functions

This paper adds monotonicity and antitonicity information to the typed lambda calculus, thereby providing a foundation for the Monotonicity Calculus first developed by van Benthem and others. We establish properties of the type system, propose a syntax, semantics, and proof calculus, and prove completeness for the calculus with respect to hierarchies of monotone and antitone functions over base preorders.

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 New One-Pass Transformation into Monadic Normal Form

2002 ◽  
Vol 9 (52) ◽  
Author(s):  
Olivier Danvy
Keyword(s):  
Normal Form ◽  
Symbolic Computation ◽  
Normal Forms ◽  
Lambda Calculus ◽  
Higher Order

We present a translation from the call-by-value lambda-calculus to monadic normal forms that includes short-cut boolean evaluation. The translation is higher-order, operates in one pass, duplicates no code, generates no chains of thunks, and is properly tail recursive. It makes a crucial use of symbolic computation at translation time.

scholarly journals Bounded Fixed Point Iteration

1991 ◽  
Vol 20 (359) ◽  
Author(s):  
Hanne Riis Nielson ◽  
Flemming Nielson
Keyword(s):  
Fixed Point ◽  
Abstract Interpretation ◽  
Higher Order ◽  
Monotone Functions ◽  
Additive Functions ◽  
Fixed Point Iteration ◽  
Exponential Bound ◽  
Strictness Analysis ◽  
Long Chains

In the context of abstract interpretation for languages without higher-order features we study the number of times a functional need to be unfolded in order to give the least fixed point. For the cases of total or monotone functions we obtain an exponential bound and in the case of strict and additive (or distributive) functions we obtain a quadratic bound. These bounds are shown to be tight in that sufficiently long chains of functions can be shown to exist. Specializing the case of strict and additive functions to functionals of a form that would correspond to iterative programs we show that a linear bound is tight. This is related to several analyses studied in the literature (including strictness analysis).

scholarly journals Experiments with ZF Set Theory in HOL and Isabelle

1995 ◽  
Vol 2 (37) ◽  
Author(s):  
Sten Agerholm ◽  
Mike Gordon
Keyword(s):  
Set Theory ◽  
Lambda Calculus ◽  
General Purpose ◽  
Higher Order ◽  
Proof Assistants ◽  
Higher Order Logic ◽  
First Order ◽  
Advantages And Disadvantages ◽  
Theory Versus

Most general purpose proof assistants support versions of<br />typed higher order logic. Experience has shown that these logics are capable<br />of representing most of the mathematical models needed in Computer<br />Science. However, perhaps there exist applications where ZF-style<br />set theory is more natural, or even necessary. Examples may include<br />Scott's classical inverse-limit construction of a model of the untyped lambda-calculus<br /> (D_inf) and the semantics of parts of the Z specification notation.<br /><br />This paper compares the representation and use of ZF set theory within<br />both HOL and Isabelle. The main case study is the construction of D_inf.<br />The advantages and disadvantages of higher-order set theory versus first-order<br />set theory are explored experimentally. This study also provides a<br />comparison of the proof infrastructure of HOL and Isabelle.

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.

Parameterizing higher-order processes on names and processes

2019 ◽  
Vol 53 (3-4) ◽  
pp. 153-206
Author(s):  
Xian Xu
Keyword(s):  
Lambda Calculus ◽  
Higher Order ◽  
The Other ◽  
First Order ◽  
Full Abstraction

Parameterization extends higher-order processes with the capability of abstraction and application (like those in lambda-calculus). As is well-known, this extension is strict, meaning that higher-order processes equipped with parameterization are strictly more expressive than those without parameterization. This paper studies strictly higher-order processes (i.e., no name-passing) with two kinds of parameterization: one on names and the other on processes themselves. We present two main results. One is that in presence of parameterization, higher-order processes can interpret first-order (name-passing) processes in a quite elegant fashion, in contrast to the fact that higher-order processes without parameterization cannot encode first-order processes at all. We present two such encodings and analyze their properties in depth, particularly full abstraction. In the other result, we provide a simpler characterization of the standard context bisimilarity for higher-order processes with parameterization, in terms of the normal bisimilarity that stems from the well-known normal characterization for higher-order calculus. As a spinoff, we show that the bisimulation up-to context technique is sound in the higher-order setting with parameterization.

scholarly journals On One-Pass CPS Transformations

2007 ◽  
Vol 14 (6) ◽  
Author(s):  
Olivier Danvy ◽  
Kevin Millikin ◽  
Lasse R. Nielsen
Keyword(s):  
Fixed Point ◽  
Normal Form ◽  
Lambda Calculus ◽  
Higher Order ◽  
The Other ◽  
Left Inverse ◽  
Post Processing ◽  
Transformation Time ◽  
Special Case ◽  
Implementation Technique

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 independently due to Appel, Danvy and Filinski, and Wand, building on Plotkin's seminal work. The other is non-compositional and based on a reduction semantics for the lambda-calculus, and is due to Sabry and Felleisen. To relate the two approaches, we use three tools: Reynolds's defunctionalization and its left inverse, refunctionalization; a special case of fold-unfold fusion due to Ohori and Sasano, fixed-point promotion; and an implementation technique for reduction semantics due to Danvy and Nielsen, refocusing.<br /> <br />This work is directly applicable to transforming programs into monadic normal form.

Sign in / Sign up

Export Citation Format

Share Document