First Class Call Stacks: Exploring Head Reduction

First Class Call Stacks: Exploring Head Reduction

Weak-head normalization is inconsistent with functional extensionality in the call-by-name λ-calculus. We explore this problem from a new angle via the conflict between extensionality and effects. Leveraging ideas from work on the λ-calculus with control, we derive and justify alternative operationa...

Full description

Bibliographic Details
Main Authors: Philip Johnson-Freyd, Paul Downen, Zena M. Ariola
Format: Article
Language:English
Published: Open Publishing Association 2016-06-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1606.06378v1
id doaj-0b85ad98050f47fea9a4c606deefa12b
record_format Article
spelling doaj-0b85ad98050f47fea9a4c606deefa12b2020-11-24T23:32:02ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802016-06-01212Proc. WoC 2015183510.4204/EPTCS.212.2:8First Class Call Stacks: Exploring Head ReductionPhilip Johnson-Freyd0Paul Downen1Zena M. Ariola2 University of Oregon University of Oregon University of Oregon Weak-head normalization is inconsistent with functional extensionality in the call-by-name λ-calculus. We explore this problem from a new angle via the conflict between extensionality and effects. Leveraging ideas from work on the λ-calculus with control, we derive and justify alternative operational semantics and a sequence of abstract machines for performing head reduction. Head reduction avoids the problems with weak-head reduction and extensionality, while our operational semantics and associated abstract machines show us how to retain weak-head reduction's ease of implementation.http://arxiv.org/pdf/1606.06378v1
collection DOAJ
language English
format Article
sources DOAJ
author Philip Johnson-Freyd
Paul Downen
Zena M. Ariola
spellingShingle Philip Johnson-Freyd
Paul Downen
Zena M. Ariola
First Class Call Stacks: Exploring Head Reduction
Electronic Proceedings in Theoretical Computer Science
author_facet Philip Johnson-Freyd
Paul Downen
Zena M. Ariola
author_sort Philip Johnson-Freyd
title First Class Call Stacks: Exploring Head Reduction
title_short First Class Call Stacks: Exploring Head Reduction
title_full First Class Call Stacks: Exploring Head Reduction
title_fullStr First Class Call Stacks: Exploring Head Reduction
title_full_unstemmed First Class Call Stacks: Exploring Head Reduction
title_sort first class call stacks: exploring head reduction
publisher Open Publishing Association
series Electronic Proceedings in Theoretical Computer Science
issn 2075-2180
publishDate 2016-06-01
description Weak-head normalization is inconsistent with functional extensionality in the call-by-name λ-calculus. We explore this problem from a new angle via the conflict between extensionality and effects. Leveraging ideas from work on the λ-calculus with control, we derive and justify alternative operational semantics and a sequence of abstract machines for performing head reduction. Head reduction avoids the problems with weak-head reduction and extensionality, while our operational semantics and associated abstract machines show us how to retain weak-head reduction's ease of implementation.
url http://arxiv.org/pdf/1606.06378v1
work_keys_str_mv AT philipjohnsonfreyd firstclasscallstacksexploringheadreduction
AT pauldownen firstclasscallstacksexploringheadreduction
AT zenamariola firstclasscallstacksexploringheadreduction
_version_ 1725535568342810624

Similar Items