On completeness of reducibility candidates as a semantics of strong normalization
This paper defines a sound and complete semantic criterion, based on reducibility candidates, for strong normalization of theories expressed in minimal deduction modulo \`a la Curry. The use of Curry-style proof-terms allows to build this criterion on the classic notion of pre-Heyting algebras and m...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2012-02-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/845/pdf |
| _version_ | 1797268706209824768 |
|---|---|
| author | Denis Cousineau |
| author_facet | Denis Cousineau |
| author_sort | Denis Cousineau |
| collection | DOAJ |
| description | This paper defines a sound and complete semantic criterion, based on
reducibility candidates, for strong normalization of theories expressed in
minimal deduction modulo \`a la Curry. The use of Curry-style proof-terms
allows to build this criterion on the classic notion of pre-Heyting algebras
and makes that criterion concern all theories expressed in minimal deduction
modulo. Compared to using Church-style proof-terms, this method provides both a
simpler definition of the criterion and a simpler proof of its completeness. |
| first_indexed | 2024-04-25T01:36:44Z |
| format | Article |
| id | doaj.art-93a4fee64fd34a23b63efc715837d3e4 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:36:44Z |
| publishDate | 2012-02-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-93a4fee64fd34a23b63efc715837d3e42024-03-08T09:27:54ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742012-02-01Volume 8, Issue 110.2168/LMCS-8(1:3)2012845On completeness of reducibility candidates as a semantics of strong normalizationDenis CousineauThis paper defines a sound and complete semantic criterion, based on reducibility candidates, for strong normalization of theories expressed in minimal deduction modulo \`a la Curry. The use of Curry-style proof-terms allows to build this criterion on the classic notion of pre-Heyting algebras and makes that criterion concern all theories expressed in minimal deduction modulo. Compared to using Church-style proof-terms, this method provides both a simpler definition of the criterion and a simpler proof of its completeness.https://lmcs.episciences.org/845/pdfcomputer science - logic in computer sciencef.4.1 |
| spellingShingle | Denis Cousineau On completeness of reducibility candidates as a semantics of strong normalization Logical Methods in Computer Science computer science - logic in computer science f.4.1 |
| title | On completeness of reducibility candidates as a semantics of strong normalization |
| title_full | On completeness of reducibility candidates as a semantics of strong normalization |
| title_fullStr | On completeness of reducibility candidates as a semantics of strong normalization |
| title_full_unstemmed | On completeness of reducibility candidates as a semantics of strong normalization |
| title_short | On completeness of reducibility candidates as a semantics of strong normalization |
| title_sort | on completeness of reducibility candidates as a semantics of strong normalization |
| topic | computer science - logic in computer science f.4.1 |
| url | https://lmcs.episciences.org/845/pdf |
| work_keys_str_mv | AT deniscousineau oncompletenessofreducibilitycandidatesasasemanticsofstrongnormalization |