Implicit automata in typed λ-calculi I: Aperiodicity in a non-commutative logic
We give a characterization of star-free languages in a λ-calculus with support for non-commutative affine types (in the sense of linear logic), via the algebraic characterization of the former using aperiodic monoids. When the type system is made commutative, we show that we get regular languages in...
| Main Authors: | , |
|---|---|
| Format: | Conference item |
| Language: | English |
| Published: |
Schloss Dagstuhl
2020
|
| _version_ | 1797065313776304128 |
|---|---|
| author | Nguyễn, LTD Pradic, P |
| author_facet | Nguyễn, LTD Pradic, P |
| author_sort | Nguyễn, LTD |
| collection | OXFORD |
| description | We give a characterization of star-free languages in a λ-calculus with support for non-commutative affine types (in the sense of linear logic), via the algebraic characterization of the former using aperiodic monoids. When the type system is made commutative, we show that we get regular languages instead. A key ingredient in our approach – that it shares with higher-order model checking – is the use of Church encodings for inputs and outputs. Our result is, to our knowledge, the first use of non-commutativity in implicit computational complexity. |
| first_indexed | 2024-03-06T21:26:51Z |
| format | Conference item |
| id | oxford-uuid:4365c369-878a-4d72-bd92-138e8f9b7368 |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-06T21:26:51Z |
| publishDate | 2020 |
| publisher | Schloss Dagstuhl |
| record_format | dspace |
| spelling | oxford-uuid:4365c369-878a-4d72-bd92-138e8f9b73682022-03-26T14:55:08ZImplicit automata in typed λ-calculi I: Aperiodicity in a non-commutative logicConference itemhttp://purl.org/coar/resource_type/c_5794uuid:4365c369-878a-4d72-bd92-138e8f9b7368EnglishSymplectic ElementsSchloss Dagstuhl2020Nguyễn, LTDPradic, PWe give a characterization of star-free languages in a λ-calculus with support for non-commutative affine types (in the sense of linear logic), via the algebraic characterization of the former using aperiodic monoids. When the type system is made commutative, we show that we get regular languages instead. A key ingredient in our approach – that it shares with higher-order model checking – is the use of Church encodings for inputs and outputs. Our result is, to our knowledge, the first use of non-commutativity in implicit computational complexity. |
| spellingShingle | Nguyễn, LTD Pradic, P Implicit automata in typed λ-calculi I: Aperiodicity in a non-commutative logic |
| title | Implicit automata in typed λ-calculi I: Aperiodicity in a non-commutative logic |
| title_full | Implicit automata in typed λ-calculi I: Aperiodicity in a non-commutative logic |
| title_fullStr | Implicit automata in typed λ-calculi I: Aperiodicity in a non-commutative logic |
| title_full_unstemmed | Implicit automata in typed λ-calculi I: Aperiodicity in a non-commutative logic |
| title_short | Implicit automata in typed λ-calculi I: Aperiodicity in a non-commutative logic |
| title_sort | implicit automata in typed λ calculi i aperiodicity in a non commutative logic |
| work_keys_str_mv | AT nguyenltd implicitautomataintypedlcalculiiaperiodicityinanoncommutativelogic AT pradicp implicitautomataintypedlcalculiiaperiodicityinanoncommutativelogic |