Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
http://hdl.handle.net/11320/7835
Tytuł: | Concatenation of Finite Sequences |
Autorzy: | Ziobro, Rafał |
Słowa kluczowe: | finite sequence finite 0-sequence concatenation |
Data wydania: | 2019 |
Data dodania: | 21-maj-2019 |
Wydawca: | DeGruyter Open |
Źródło: | Formalized Mathematics, Volume 27, Issue 1, Pages 1-13 |
Abstrakt: | The coexistence of “classical” finite sequences [1] and their zero-based equivalents finite 0-sequences [6] in Mizar has been regarded as a disadvantage. However the suggested replacement of the former type with the latter [5] has not yet been implemented, despite of several advantages of this form, such as the identity of length and domain operators [4]. On the other hand the number of theorems formalized using finite sequence notation is much larger then of those based on finite 0-sequences, so such translation would require quite an effort. The paper addresses this problem with another solution, using the Mizar system [3], [2]. Instead of removing one notation it is possible to introduce operators which would concatenate sequences of various types, and in this way allow utilization of the whole range of formalized theorems. While the operation could replace existing FS2XFS, XFS2FS commands (by using empty sequences as initial elements) its universal notation (independent on sequences that are concatenated to the initial object) allows to “forget” about the type of sequences that are concatenated on further positions, and thus simplify the proofs. |
Afiliacja: | Department of Carbohydrate Technology, University of Agriculture, Krakow, Poland |
URI: | http://hdl.handle.net/11320/7835 |
DOI: | 10.2478/forma-2019-0001 |
ISSN: | 1426-2630 |
e-ISSN: | 1898-9934 |
metadata.dc.identifier.orcid: | 0000-0001-9681-4380 |
Typ Dokumentu: | Article |
Występuje w kolekcji(ach): | Formalized Mathematics, 2019, Volume 27, Issue 1 |
Pliki w tej pozycji:
Plik | Opis | Rozmiar | Format | |
---|---|---|---|---|
forma_2019_27_1_001.pdf | 250,4 kB | Adobe PDF | Otwórz |
Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL