NDLI logo
  • Content
  • Similar Resources
  • Metadata
  • Cite This
  • Log-in
  • Fullscreen
Log-in
Do not have an account? Register Now
Forgot your password? Account recovery
  1. Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (CSL-LICS '14)
  2. Beta reduction is invariant, indeed
Loading...

Please wait, while we are loading the content...

Trade-off analysis meets probabilistic model checking
Understanding biology through logic
The Ackermann award 2014
Infinite-state energy games
Abstract interpretation: past, present and future
Computer-checked mathematics: a formal proof of the odd order theorem
Citations for the test-of-time award from 1994
Beta reduction is invariant, indeed
Regular combinators for string transformations
Asymptotic behaviour in temporal logic
Weight monitoring with linear temporal logic: complexity and decidability
Graph logics with rational relations: the role of word combinatorics
Effective interpolation and preservation in guarded logics
On the discriminating power of passivation and higher-order interaction
A domain-theoretic approach to Brownian motion and general continuous stochastic processes
Two-way cost automata and cost logics over infinite trees
Decomposition theorems and model-checking for the modal μ-calculus
Logic for communicating automata with parameterized topology
Logical characterization of weighted pebble walking automata
Coinduction up-to in a fibrational setting
Model checking existential logic on partially ordered sets
Zero-reachability in probabilistic multi-counter automata
The complexity of admissibility in Omega-regular games
On the characterization of models of H
A decision procedure for satisfiability in separation logic with inductive predicates
Secure equilibria in weighted games
Weak MSO: automata and expressiveness modulo bisimilarity
Symmetry in concurrent games
Decidability of weak logics with deterministic transitive closure
Equality and fixpoints in the calculus of structures
The tractability frontier of graph-like first-order query sets
One hierarchy spawns another: graph deconstructions and the complexity classification of conjunctive queries
On the total variation distance of labelled Markov chains
System F with coercion constraints
The geometry of synchronization
On the pigeonhole and related principles in deep inference and monotone systems
Expressive completeness of separation logic with two variables and no separating conjunction
A new correctness criterion for MLL proof nets
On periodically iterated morphisms
Pattern logics and auxiliary relations
Substitution, jumps, and algebraic effects
Satisfiability modulo counting: a new approach for analyzing privacy properties
Achieving new upper bounds for the hypergraph duality problem through logic
KAT + B!
Symmetric normalisation for intuitionistic logic
Equilibria of concurrent games on event structures
Subclasses of presburger arithmetic and the weak EXP hierarchy
Senescent ground tree rewrite systems
Preservation and decomposition theorems for bounded degree structures
No proof nets for MLL with units: proof equivalence in MLL is PSPACE-complete
Abstract interpretation from Büchi automata
Memoryful geometry of interaction: from coalgebraic components to algebraic effects
Axioms and decidability for type isomorphism in the presence of sums
Functional reactive types
Probably safe or live
A quest for algorithmically random infinite structures
On the succinctness of query rewriting over shallow ontologies
Turing machines with atoms, constraint satisfaction problems, and descriptive complexity
Local temporal reasoning
On Hanf-equivalence and the number of embeddings of small induced subgraphs
Non-elementary complexities for branching VASS, MELL, and extensions
Infinite sequential games with real-valued payoffs
Hyper-Ackermannian bounds for pushdown vector addition systems
Transition systems over games
Compositional verification of termination-preserving refinement of concurrent programs
Eilenberg-MacLane spaces in homotopy type theory
MSO queries on trees: enumerating answers under updates
On the computing power of +, -, and ×
On the Hoare theory of monadic recursion schemes
Formulae-as-types for an involutive negation
A type theory for productive coprogramming via guarded recursion
Deadlock and lock freedom in the linear π-calculus
On context semantics and interaction nets
Anchored LTL separation
Separating regular languages with first-order logic
Logics with counting and equivalence
A functional functional interpretation
Compositional higher-order model checking via ω-regular games over Böhm trees
Finite-memory strategy synthesis for robust multidimensional mean-payoff objectives
Faster decision of first-order graph properties

Similar Documents

...
Beta Reduction is Invariant, Indeed

Article

...
Beta Reduction is Invariant, Indeed (Long Version) (2014)

...
Beta Reduction is Invariant , Indeed Beniamino Accattoli

Article

...
Explicit substitutions in the reduction of lambda terms

Article

...
An overview of λ-calculus sharing graph reduction (1999).

...
Explicit substitutions calculi with one step eta-reduction decided explicitly.

Article

...
Efficiency of λ-calculi with explicit substitutions (1996)

Article

...
Is the Optimal Implementation Inefficient? Elementarily Not

Article

...
Generalised Beta-Reduction and Explicit Substitutions (1996)

Article

Beta reduction is invariant, indeed

Content Provider ACM Digital Library
Author Accattoli, Beniamino Dal Lago, Ugo
Abstract Slot and van Emde Boas' weak invariance thesis states that reasonable machines can simulate each other within a polynomially overhead in time. Is λ-calculus a reasonable machine? Is there a way to measure the computational complexity of a λ-term? This paper presents the first complete positive answer to this long-standing problem. Moreover, our answer is completely machine-independent and based over a standard notion in the theory of λ-calculus: the length of a leftmost-outermost derivation to normal form is an invariant cost model. Such a theorem cannot be proved by directly relating λ-calculus with Turing machines or random access machines, because of the size explosion problem: there are terms that in a linear number of steps produce an exponentially long output. The first step towards the solution is to shift to a notion of evaluation for which the length and the size of the output are linearly related. This is done by adopting the linear substitution calculus (LSC), a calculus of explicit substitutions modelled after linear logic proof nets and admitting a decomposition of leftmost-outermost derivations with the desired property. Thus, the LSC is invariant with respect to, say, random access machines. The second step is to show that LSC is invariant with respect to the λ-calculus. The size explosion problem seems to imply that this is not possible: having the same notions of normal form, evaluation in the LSC is exponentially longer than in the λ-calculus. We solve such an impasse by introducing a new form of shared normal form and shared reduction, deemed useful. Useful evaluation avoids those steps that only unshare the output without contributing to β-redexes, i.e. the steps that cause the blow-up in size. The main technical contribution of the paper is indeed the definition of useful reductions and the thorough analysis of their properties.
Starting Page 1
Ending Page 10
Page Count 10
File Format PDF
ISBN 9781450328869
DOI 10.1145/2603088.2603105
Language English
Publisher Association for Computing Machinery (ACM)
Publisher Date 2014-07-14
Publisher Place New York
Access Restriction Subscribed
Subject Keyword Λ-calculus Explicit substitutions Sharing Cost models Computational complexity
Content Type Text
Resource Type Article
  • About
  • Disclaimer
  • Feedback
  • Sponsor
  • Contact
  • Chat with Us
About National Digital Library of India (NDLI)
NDLI logo

National Digital Library of India (NDLI) is a virtual repository of learning resources which is not just a repository with search/browse facilities but provides a host of services for the learner community. It is sponsored and mentored by Ministry of Education, Government of India, through its National Mission on Education through Information and Communication Technology (NMEICT). Filtered and federated searching is employed to facilitate focused searching so that learners can find the right resource with least effort and in minimum time. NDLI provides user group-specific services such as Examination Preparatory for School and College students and job aspirants. Services for Researchers and general learners are also provided. NDLI is designed to hold content of any language and provides interface support for 10 most widely used Indian languages. It is built to provide support for all academic levels including researchers and life-long learners, all disciplines, all popular forms of access devices and differently-abled learners. It is designed to enable people to learn and prepare from best practices from all over the world and to facilitate researchers to perform inter-linked exploration from multiple sources. It is developed, operated and maintained from Indian Institute of Technology Kharagpur.

Learn more about this project from here.

Disclaimer

NDLI is a conglomeration of freely available or institutionally contributed or donated or publisher managed contents. Almost all these contents are hosted and accessed from respective sources. The responsibility for authenticity, relevance, completeness, accuracy, reliability and suitability of these contents rests with the respective organization and NDLI has no responsibility or liability for these. Every effort is made to keep the NDLI portal up and running smoothly unless there are some unavoidable technical issues.

Feedback

Sponsor

Ministry of Education, through its National Mission on Education through Information and Communication Technology (NMEICT), has sponsored and funded the National Digital Library of India (NDLI) project.

Contact National Digital Library of India
Central Library (ISO-9001:2015 Certified)
Indian Institute of Technology Kharagpur
Kharagpur, West Bengal, India | PIN - 721302
See location in the Map
03222 282435
Mail: support@ndl.gov.in
Sl. Authority Responsibilities Communication Details
1 Ministry of Education (GoI),
Department of Higher Education
Sanctioning Authority https://www.education.gov.in/ict-initiatives
2 Indian Institute of Technology Kharagpur Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project https://www.iitkgp.ac.in
3 National Digital Library of India Office, Indian Institute of Technology Kharagpur The administrative and infrastructural headquarters of the project Dr. B. Sutradhar  bsutra@ndl.gov.in
4 Project PI / Joint PI Principal Investigator and Joint Principal Investigators of the project Dr. B. Sutradhar  bsutra@ndl.gov.in
Prof. Saswat Chakrabarti  will be added soon
5 Website/Portal (Helpdesk) Queries regarding NDLI and its services support@ndl.gov.in
6 Contents and Copyright Issues Queries related to content curation and copyright issues content@ndl.gov.in
7 National Digital Library of India Club (NDLI Club) Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach clubsupport@ndl.gov.in
8 Digital Preservation Centre (DPC) Assistance with digitizing and archiving copyright-free printed books dpc@ndl.gov.in
9 IDR Setup or Support Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops idr@ndl.gov.in
I will try my best to help you...
Cite this Content
Loading...