Journal article 1200 views
A domain model characterising strong normalisation
Annals of Pure and Applied Logic, Volume: 156, Issue: 1, Pages: 39 - 50
Swansea University Author: Ulrich Berger
Full text not available from this repository: check for access using links below.
DOI (Published version): 10.1016/j.apal.2008.06.005
Abstract
Building on previous work by Coquand and Spiwack we construct a strict domain-theoretic model for the untyped lambda-calculus with pattern matching and term rewriting which has the property that a term is strongly normalising if its value is not bottom. There are no disjointness or confluence condit...
Published in: | Annals of Pure and Applied Logic |
---|---|
ISSN: | 0168-0072 |
Published: |
2008
|
Online Access: |
Check full text
|
URI: | https://cronfa.swan.ac.uk/Record/cronfa128 |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
Abstract: |
Building on previous work by Coquand and Spiwack we construct a strict domain-theoretic model for the untyped lambda-calculus with pattern matching and term rewriting which has the property that a term is strongly normalising if its value is not bottom. There are no disjointness or confluence conditions imposed on the rewrite rules, and under a mild but necessary condition completeness of the method is proven. As an application, we prove strong normalisation for barrecursion in higher types combined with polymorphism and non-deterministic choice. |
---|---|
Keywords: |
lambda-calculus, term rewriting, normalisation, domain theory |
College: |
Faculty of Science and Engineering |
Issue: |
1 |
Start Page: |
39 |
End Page: |
50 |