| 1. |
- Bernardy, Jean-Philippe, 1978, et al.
(författare)
-
Assessing the Unitary RNN as an End-to-End Compositional Model of Syntax
- 2022
-
Ingår i: EPTCS 366. Proceedings End-to-End Compositional Models of Vector-Based Semantics, NUI Galway, 15-16 August, 2022, edited by: Michael Moortgat and Gijs Wijnholds. - Waterloo, Australia : Open Publishing Association. - 2075-2180.
-
Konferensbidrag (refereegranskat)abstract
- We show that both an LSTM and a unitary-evolution recurrent neural network (URN) can achieve encouraging accuracy on two types of syntactic patterns: context-free long distance agreement, and mildly context-sensitive cross serial dependencies. This work extends recent experiments on deeply nested context-free long distance dependencies, with similar results. URNs differ from LSTMs in that they avoid non-linear activation functions, and they apply matrix multiplication to word embeddings encoded as unitary matrices. This permits them to retain all information in the processing of an input string over arbitrary distances. It also causes them to satisfy strict compositionality. URNs constitute a significant advance in the search for explainable models in deep learning applied to NLP.
|
|
| 2. |
- Curzi, Gianluca, 1991
(författare)
-
Linear Additives
- 2021
-
Ingår i: Electronic Proceedings in Theoretical Computer Science (EPTCS). - 2075-2180.
-
Tidskriftsartikel (refereegranskat)abstract
- We introduce LAM, a subsystem of IMALL2 with restricted additive rules able to manage duplication linearly, called linear additive rules. LAM is presented as the type assignment system for a calculus endowed with copy constructors, which deal with substitution in a linear fashion. As opposed to the standard additive rules, the linear additive rules do not affect the complexity of term reduction: typable terms of LAM enjoy linear strong normalization. Moreover, a mildly weakened version of cut-elimination for this system is proven which takes a cubic number of steps. Finally, we define a sound translation from LAM’s proofs into IMLL2’s linear lambda terms, and we study its complexity.
|
|
| 3. |
- Johansson, Moa, 1981, et al.
(författare)
-
Conjectures, tests and proofs: An overview of theory exploration
- 2021
-
Ingår i: Electronic Proceedings in Theoretical Computer Science, EPTCS. - 2075-2180. ; 341, s. 1-16
-
Konferensbidrag (refereegranskat)abstract
- A key component of mathematical reasoning is the ability to formulate interesting conjectures about a problem domain at hand. In this paper, we give a brief overview of a theory exploration system called QuickSpec, which is able to automatically discover interesting conjectures about a given set of functions. QuickSpec works by interleaving term generation with random testing to form candidate conjectures. This is made tractable by starting from small sizes and ensuring that only terms that are irreducible with respect to already discovered conjectures are considered. QuickSpec has been successfully applied to generate lemmas for automated inductive theorem proving as well as to generate specifications of functional programs. We give an overview of typical use-cases of QuickSpec, as well as demonstrating how to easily connect it to a theorem prover of the user’s choice.
|
|
| 4. |
|
|
| 5. |
- Spengler, Stephan, et al.
(författare)
-
TSO Games : On the decidability of safety games under the total store order semantics
- 2023
-
Ingår i: Electronic Proceedings in Theoretical Computer Science. - : EPTCSorg. - 2075-2180. ; 390, s. 82-98
-
Tidskriftsartikel (refereegranskat)abstract
- We consider an extension of the classical Total Store Order (TSO) semantics by expanding it to turn-based 2-player safety games. During her turn, a player can select any of the communicating processes and perform its next transition. We consider different formulations of the safety game problem depending on whether one player or both of them transfer messages from the process buffers to the shared memory. We give the complete decidability picture for all the possible alternatives.
|
|
