Journal article 1216 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 |