Showing 1–9 of 9 results for author: Gajda, M J

Computational philosophy of science

Authors: Michał J. Gajda

Abstract: Philosophy of science attempts to describe all parts of the scientific process in a general way in order to facilitate the description, execution and improvements of this process. So far, all proposed philosophies have only covered existing processes and disciplines partially and imperfectly. In particular logical approaches have always received a lot of attention due to attempts to fundamentall… ▽ More Philosophy of science attempts to describe all parts of the scientific process in a general way in order to facilitate the description, execution and improvements of this process. So far, all proposed philosophies have only covered existing processes and disciplines partially and imperfectly. In particular logical approaches have always received a lot of attention due to attempts to fundamentally address issues with the definition of science as a discipline with reductionist theories. We propose a new way to approach the problem from the perspective of computational complexity and argue why this approach may be better than previous propositions based on pure logic and mathematics. △ Less

Submitted 4 February, 2023; originally announced February 2023.

Comments: Draft under review

MSC Class: 03A10; 03D15; 03A05 ACM Class: F.4.1; I.4.2; I.2.0; I.2.6

Data accounting and error counting

Authors: Michał J. Gajda

Abstract: Can we infer sources of errors from outputs of the complex data analytics software? Bidirectional programming promises that we can reverse flow of software, and translate corrections of output into corrections of either input or data analysis. This allows us to achieve holy grail of automated approaches to debugging, risk reporting and large scale distributed error tracking. Since processing… ▽ More Can we infer sources of errors from outputs of the complex data analytics software? Bidirectional programming promises that we can reverse flow of software, and translate corrections of output into corrections of either input or data analysis. This allows us to achieve holy grail of automated approaches to debugging, risk reporting and large scale distributed error tracking. Since processing of risk reports and data analysis pipelines can be frequently expressed using a sequence relational algebra operations, we propose a replacement of this traditional approach with a data summarization algebra that helps to determine an impact of errors. It works by defining data analysis of a necessarily complete summarization of a dataset, possibly in multiple ways along multiple dimensions. We also present a description to better communicate how the complete summarizations of the input data may facilitates easier debugging and more efficient development of analysis pipelines. This approach can also be described as an generalization of axiomatic theories of accounting into data analytics, thus dubbed data accounting. We also propose formal properties that allow for transparent assertions about impact of individual records on the aggregated data and ease debugging by allowing to find minimal changes that change behaviour of data analysis on per-record basis. △ Less

Submitted 29 January, 2023; originally announced January 2023.

Comments: In press

ACM Class: H.1.1; J.1; I.1.3; H.2.3; H.4.2; B.4.5; F.4.m

Journal ref: Analytics in Finance and Risk Management 2024

Consistent ultrafinitist logic

Authors: Michał J. Gajda

Abstract: Ultrafinitism postulates that we can only compute on relatively short objects, and numbers beyond certain value are not available. This approach would also forbid many forms of infinitary reasoning and allow to remove certain paradoxes stemming from enumeration theorems. However, philosophers still disagree of whether such a finitist logic would be consistent. We present preliminary work on a proo… ▽ More Ultrafinitism postulates that we can only compute on relatively short objects, and numbers beyond certain value are not available. This approach would also forbid many forms of infinitary reasoning and allow to remove certain paradoxes stemming from enumeration theorems. However, philosophers still disagree of whether such a finitist logic would be consistent. We present preliminary work on a proof system based on Curry-Howard isomorphism. We also try to present some well-known theorems that stop being true in such systems, whereas opposite statements become provable. This approach presents certain impossibility results as logical paradoxes stemming from a profligate use of transfinite reasoning. △ Less

Submitted 2 June, 2024; v1 submitted 24 June, 2021; originally announced June 2021.

Comments: Under review

Report number: 01 MSC Class: 03A05; 03D10; 03D25; 03F40; 03F50; 03F55 ACM Class: F.4.1; F.1.1

Journal ref: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2023.5

Curious properties of latency distributions

Authors: Michał J. Gajda

Abstract: Network latency distributions, their algebra, and use examples. This paper considers modeling of capacity-insensitive processes and distributed systems. It provides algebraic properties of the latency distribution algebra and Haskell code to implement the model. Network latency distributions, their algebra, and use examples. This paper considers modeling of capacity-insensitive processes and distributed systems. It provides algebraic properties of the latency distribution algebra and Haskell code to implement the model. △ Less

Submitted 5 November, 2020; originally announced November 2020.

Infer XPath

Authors: Michał J. Gajda, Hai Nguyen Quang, Do Ngoc Khanh, Vuong Hai Thanh

Abstract: We propose reformulation of discovery of data structure within a web page as relations between sets of document nodes. We start by reformulating web page analysis as finding expressions in extension of XPath. Then we propose to automatically discover these XPath expressions with InferXPath meta-language. Our goal is to automate laborious process of conversion of manually created web pages that ser… ▽ More We propose reformulation of discovery of data structure within a web page as relations between sets of document nodes. We start by reformulating web page analysis as finding expressions in extension of XPath. Then we propose to automatically discover these XPath expressions with InferXPath meta-language. Our goal is to automate laborious process of conversion of manually created web pages that serve as software documentations, wikis, and reference documents, and speed up their conversion into tabular data that can be directly fed into data pipeline. △ Less

Submitted 5 November, 2020; originally announced November 2020.

Less Arbitrary waiting time

Authors: Michał J. Gajda

Abstract: Property testing is the cheapest and most precise way of building up a test suite for your program. Especially if the datatypes enjoy nice mathematical laws. But it is also the easiest way to make it run for an unreasonably long time. We prove connection between deeply recursive data structures, and epidemic growth rate, and show how to fix the problem, and make Arbitrary instances run in linear t… ▽ More Property testing is the cheapest and most precise way of building up a test suite for your program. Especially if the datatypes enjoy nice mathematical laws. But it is also the easiest way to make it run for an unreasonably long time. We prove connection between deeply recursive data structures, and epidemic growth rate, and show how to fix the problem, and make Arbitrary instances run in linear time with respect to assumed test size. △ Less

Submitted 12 January, 2021; v1 submitted 5 November, 2020; originally announced November 2020.

Fast XML/HTML for Haskell: XML TypeLift

Authors: Michał J. Gajda, Dmitry Krylov

Abstract: The paper presents and compares a range of parsers with and without data mapping for conversion between XML and Haskell. The best performing parser competes favorably with the fastest tools available in other languages and is, thus, suitable for use in large-scale data analysis. The best performing parser also allows software developers of intermediate-level Haskell programming skills to start pro… ▽ More The paper presents and compares a range of parsers with and without data mapping for conversion between XML and Haskell. The best performing parser competes favorably with the fastest tools available in other languages and is, thus, suitable for use in large-scale data analysis. The best performing parser also allows software developers of intermediate-level Haskell programming skills to start processing large numbers of XML documents soon after finding the relevant XML Schema from a simple internet search, without the need for specialist prior knowledge or skills. We hope that this unique combination of parser performance and usability will provide a new standard for XML mapping to high-level languages. △ Less

Submitted 5 November, 2020; originally announced November 2020.

Towards a more perfect union type

Authors: Michał J. Gajda

Abstract: We present a principled theoretical framework for inferring and checking the union types, and show its work in practice on JSON data structures. The framework poses a union type inference as a learning problem from multiple examples. The categorical framework is generic and easily extensible. We present a principled theoretical framework for inferring and checking the union types, and show its work in practice on JSON data structures. The framework poses a union type inference as a learning problem from multiple examples. The categorical framework is generic and easily extensible. △ Less

Submitted 12 January, 2021; v1 submitted 5 November, 2020; originally announced November 2020.

Multicloud API binding generation from documentation

Authors: Michał J. Gajda, Vitor Vitali Barrozzi, Gabriel Araujo

Abstract: We present industry experience from implementing retargetable cloud API binding generator. The analysis is implemented in Haskell, using type classes, types a la carte, and code generation monad. It also targets Haskell, and allows us to bind cloud APIs on short notice, and unprecedented scale. We present industry experience from implementing retargetable cloud API binding generator. The analysis is implemented in Haskell, using type classes, types a la carte, and code generation monad. It also targets Haskell, and allows us to bind cloud APIs on short notice, and unprecedented scale. △ Less

Submitted 5 November, 2020; originally announced November 2020.

Comments: Presented on XP 2020: Agility in Microservices workshop