Standardization and conservativity of a refined call-by-value lambda-calculus

Giulio Guerrieri, Luca Paolini, Simona Ronchi Della Rocca

Research output: Contribution to journalArticlepeer-review

7 Citations (Scopus)

Abstract

We study an extension of Plotkin’s call-by-value lambda-calculus via two commutation rules (sigma-reductions). These commutation rules are sufficient to remove harmful call-by-value normal forms from the calculus, so that it enjoys elegant characteriza- tions of many semantic properties. We prove that this extended calculus is a conservative refinement of Plotkin’s one. In particular, the notions of solvability and potential valuability for this calculus coincide with those for Plotkin’s call-by-value lambda-calculus. The proof rests on a standardization theorem proved by generalizing Takahashi’s approach of parallel reductions to our set of reduction rules. The standardization is weak (i.e. redexes are not fully sequentialized) because of overlapping interferences between reductions.

Original languageEnglish
Article number29
JournalLogical Methods in Computer Science
Volume13
Issue number4
Early online date22 Dec 2017
DOIs
Publication statusPublished - 22 Dec 2017

Keywords

  • Call-by-value
  • Head reduction
  • Internal reduction
  • Lambda-calculus
  • Observational equivalence
  • Parallel reduction
  • Potential valuability
  • Sequentialization
  • Sigma- reduction
  • Solv- ability
  • Standard sequence
  • Standardization

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Standardization and conservativity of a refined call-by-value lambda-calculus'. Together they form a unique fingerprint.

Cite this