New equations for neutral terms: a sound and complete decision procedure, formalized

Guillaume Allais; Conor McBride; Pierre Boutillier

doi:10.1145/2502409.2502411

New equations for neutral terms: a sound and complete decision procedure, formalized

Guillaume Allais, Conor McBride, Pierre Boutillier

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution book

12 Citations (Scopus)

23 Downloads (Pure)

Abstract

The definitional equality of an intensional type theory is its test of type compatibility. Today's systems rely on ordinary evaluation semantics to compare expressions in types, frustrating users with type errors arising when evaluation fails to identify two `obviously' equal terms. If only the machine could decide a richer theory! We propose a way to decide theories which supplement evaluation with `ν-rules', rearranging the neutral parts of normal forms, and report a successful initial experiment.

We study a simple λ-calculus with primitive fold, map and append operations on lists and develop in Agda a sound and complete decision procedure for an equational theory enriched with monoid, functor and fusion laws.

Original language	English
Title of host publication	DTP '13: Proceedings of the 2013 ACM SIGPLAN workshop on Dependently-typed programming
Place of Publication	New York
Pages	13-24
Number of pages	12
DOIs	https://doi.org/10.1145/2502409.2502411
Publication status	Published - 24 Sept 2013

Keywords

normalization by evaluation
logical relations
simply typed lambda calculus
map fusion

Access to Document

10.1145/2502409.2502411

Allais-etal-DTP2013-New-equations-for-neutral-termsAccepted author manuscript, 840 KBLicence: Strath_1

Cite this

@inproceedings{4357b693f1e0443a8672743d044cb5b5,

title = "New equations for neutral terms: a sound and complete decision procedure, formalized",

abstract = "The definitional equality of an intensional type theory is its test of type compatibility. Today's systems rely on ordinary evaluation semantics to compare expressions in types, frustrating users with type errors arising when evaluation fails to identify two `obviously' equal terms. If only the machine could decide a richer theory! We propose a way to decide theories which supplement evaluation with `ν-rules', rearranging the neutral parts of normal forms, and report a successful initial experiment. We study a simple λ-calculus with primitive fold, map and append operations on lists and develop in Agda a sound and complete decision procedure for an equational theory enriched with monoid, functor and fusion laws.",

keywords = "normalization by evaluation, logical relations, simply typed lambda calculus, map fusion",

author = "Guillaume Allais and Conor McBride and Pierre Boutillier",

year = "2013",

month = sep,

day = "24",

doi = "10.1145/2502409.2502411",

language = "English",

isbn = "9781450323840",

pages = "13--24",

booktitle = "DTP '13: Proceedings of the 2013 ACM SIGPLAN workshop on Dependently-typed programming",

}

TY - GEN

T1 - New equations for neutral terms

T2 - a sound and complete decision procedure, formalized

AU - Allais, Guillaume

AU - McBride, Conor

AU - Boutillier, Pierre

PY - 2013/9/24

Y1 - 2013/9/24

N2 - The definitional equality of an intensional type theory is its test of type compatibility. Today's systems rely on ordinary evaluation semantics to compare expressions in types, frustrating users with type errors arising when evaluation fails to identify two `obviously' equal terms. If only the machine could decide a richer theory! We propose a way to decide theories which supplement evaluation with `ν-rules', rearranging the neutral parts of normal forms, and report a successful initial experiment. We study a simple λ-calculus with primitive fold, map and append operations on lists and develop in Agda a sound and complete decision procedure for an equational theory enriched with monoid, functor and fusion laws.

AB - The definitional equality of an intensional type theory is its test of type compatibility. Today's systems rely on ordinary evaluation semantics to compare expressions in types, frustrating users with type errors arising when evaluation fails to identify two `obviously' equal terms. If only the machine could decide a richer theory! We propose a way to decide theories which supplement evaluation with `ν-rules', rearranging the neutral parts of normal forms, and report a successful initial experiment. We study a simple λ-calculus with primitive fold, map and append operations on lists and develop in Agda a sound and complete decision procedure for an equational theory enriched with monoid, functor and fusion laws.

KW - normalization by evaluation

KW - logical relations

KW - simply typed lambda calculus

KW - map fusion

UR - https://arxiv.org/abs/1304.0809

U2 - 10.1145/2502409.2502411

DO - 10.1145/2502409.2502411

M3 - Conference contribution book

SN - 9781450323840

SP - 13

EP - 24

BT - DTP '13: Proceedings of the 2013 ACM SIGPLAN workshop on Dependently-typed programming

CY - New York

ER -

New equations for neutral terms: a sound and complete decision procedure, formalized

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this