Related papers: Crumbling Abstract Machines
In order to achieve competitive performance, abstract machines for Prolog and related languages end up being large and intricate, and incorporate sophisticated optimizations, both at the design and at the implementation levels. At the same…
We address the problem of complementing higher-order patterns without repetitions of existential variables. Differently from the first-order case, the complement of a pattern cannot, in general, be described by a pattern, or even by a…
Algorithm extraction aims to synthesize executable programs directly from models trained on algorithmic tasks, enabling de novo algorithm discovery without relying on human-written code. However, applying this paradigm to Transformer is…
Large Language Models (LLMs) often struggle with deductive judgment in syllogistic reasoning, systematically conflating semantic plausibility with formal validity a phenomenon known as content effect. This bias persists even when models…
We are entering a new era in which software systems are becoming more and more complex and larger. So, the composition of such systems is becoming infeasible by manual means. To address this challenge, self-organising software models…
We propose a decision-theoretic framework for computational complexity, complementary to classical theory: moving from syntactic exactness (Turing / Shannon) to semantic simulability (Le Cam). While classical theory classifies problems by…
Human intelligence relies in part on our brains' ability to create abstract mental models that succinctly capture the hidden blueprint of our reality. Such abstract world models notably allow us to rapidly navigate novel situations by…
Parameterization extends higher-order processes with the capability of abstraction (akin to that in lambda-calculus), and is known to be able to enhance the expressiveness. This paper focuses on the parameterization of names, i.e. a…
Designing scalable estimation algorithms is a core challenge in modern statistics. Here we introduce a framework to address this challenge based on parallel approximants, which yields estimators with provable properties that operate on the…
The two Girard translations provide two different means of obtaining embeddings of Intuitionistic Logic into Linear Logic, corresponding to different lambda-calculus calling mechanisms. The translations, mapping A -> B respectively to !A -o…
The logic programming paradigm provides the basis for a new intensional view of higher-order notions. This view is realized primarily by employing the terms of a typed lambda calculus as representational devices and by using a richer form…
Weak-head normalization is inconsistent with functional extensionality in the call-by-name $\lambda$-calculus. We explore this problem from a new angle via the conflict between extensionality and effects. Leveraging ideas from work on the…
Variable sharing is a fundamental property in the static analysis of logic programs, since it is instrumental for ensuring correctness and increasing precision while inferring many useful program properties. Such properties include modes,…
Substructural type systems, such as affine (and linear) type systems, are type systems which impose restrictions on copying (and discarding) of variables, and they have found many applications in computer science, including quantum…
We give a formal treatment of simple type theories, such as the simply-typed $\lambda$-calculus, using the framework of abstract clones. Abstract clones traditionally describe first-order structures, but by equipping them with additional…
The lambda calculus is a widely accepted computational model of higher-order functional pro- grams, yet there is not any direct and universally accepted cost model for it. As a consequence, the computational difficulty of reducing lambda…
The field of quantum computing is at an exciting time where we are constructing novel hardware, evaluating algorithms, and finding out what works best. As qubit technology grows and matures, we need to be ready to design and program larger…
Many interpretable AI approaches have been proposed to provide plausible explanations for a model's decision-making. However, configuring an explainable model that effectively communicates among computational modules has received less…
Abstraction is a powerful idea widely used in science, to model, reason and explain the behavior of systems in a more tractable search space, by omitting irrelevant details. While notions of abstraction have matured for deterministic…
We prove that orthogonal constructor term rewrite systems and lambda-calculus with weak (i.e., no reduction is allowed under the scope of a lambda-abstraction) call-by-value reduction can simulate each other with a linear overhead. In…