Multimodal systems and Large Language Models have shown remarkable capabilities in text-based reasoning, yet their capacity to perceive and interpret visual art remains uncertain. This study examines how CLIP “sees” and understands artworks by comparing their responses to human- and AI-generated paintings in the European tradition from the Renaissance onward. The analysis focuses on its ability to identify style, period and cultural context, as well as potential biases in its perception, evaluated against human judgments.

Abstract The Copernicus Regional Reanalysis for Europe, CERRA, is a high-resolution regional reanalysis dataset for the European domain. In recent years, it has shown significant utility across various climate-related tasks, ranging from forecasting and climate change research to renewable energy prediction, resource management, air quality risk assessment, and the forecasting of rare events, among others. Unfortunately, the availability of CERRA is lagging 2 years behind the current date, due to constraints in acquiring the requisite external data and the intensive computational demands inherent in its generation. As a solution, this paper introduces a novel method using diffusion models to approximate CERRA downscaling in a data-driven manner, without additional informations. By leveraging the lower resolution ERA5 dataset, which provides boundary conditions for CERRA, we approach this as a super-resolution task. Focusing on wind speed around Italy, our model, trained on existing CERRA data, shows promising results, closely mirroring the original CERRA. Validation with in-situ observations further confirms the model’s accuracy in approximating ground measurements.

Abstract Different encodings of datapoints in the latent space of latent-vector generative models may result in more or less effective and disentangled characterizations of the different explanatory factors of variation behind the data. Many works have been recently devoted to the exploration of the latent space of specific models, mostly focused on the study of how features are disentangled and of how trajectories producing desired alterations of data in the visible space can be found. In this work we address the more general problem of comparing the latent spaces of different models, looking for transformations between them. We confined the investigation to the familiar and largely investigated case of generative models for the data manifold of human faces. The surprising, preliminary result reported in this article is that (provided models have not been taught or explicitly conceived to act differently) a simple linear mapping is enough to pass from a latent space to another while preserving most of the information. This is full of consequences for representation learning, potentially paving the way to the transformation of editing trajectories from one space to another, or the adaptation of disentanglement techniques between different generative domains.

This paper is a report of our extensive experimentation, during the last two years, of deep reinforcement techniques for training an agent to move in the dungeons of the famous Rogue video game. The challenging nature of the problem is tightly related to the procedural, random generation of new dungeon maps at each level, which forbids any form of level-specific learning and forces us to address the navigation problem in its full generality. Other interesting aspects of the game from the point of view of automatic learning are the partially observable nature of the problem since maps are initially not visible and get discovered during exploration, and the problem of sparse rewards, requiring the acquisition of complex, nonreactive behaviors involving memory and planning. In this paper, we develop on previous works to make a more systematic comparison of different learning techniques, focusing in particular on Asynchronous Advantage Actor-Critic and Actor-Critic with Experience Replay (ACER). In a game like Rogue, sparsity of rewards is mitigated by the variability of the dungeon configurations (sometimes, by luck, exit is at hand); if this variability can be tamed-as ACER, better than other algorithms, seems able to do-the problem of sparse rewards can be overcome without any need of intrinsic motivations.

Blum's speedup theorem is a major theorem in computational complexity, showing the existence of computable functions for which no optimal program can exist: for any speedup function r there exists a function fr such that for any program computing fr we can find an alternative program computing it with the desired speedup r. The main corollary is that algorithmic problems do not have, in general, a inherent complexity.

We address computational complexity writing polymorphic functions between finite types (i.e., types with a finite number of canonical elements), expressing costs in terms of the cardinality of these types. This allows us to rediscover, in a more syntactical setting, the known result that the different levels in the hierarchy of higher-order primitive recursive functions (Gödel system T), when interpreted over finite structures, precisely capture basic complexity classes: functions of rank 1 characterize LOGSPACE, rank 2 PTIME, rank 3 PSPACE, rank 4 EXPTIME = DTIME(2 poly ), and so on.

A new “inductive” approach to standardization for the λ-calculus has been recently introduced by Xi, allowing him to establish a double-exponential upper bound |M|2|σ|for the length of the standard reduction relative to an arbitrary reduction σ originated in M. In this paper we refine Xi's analysis, obtaining much better bounds, especially for computations producing small normal forms. For instance, for terms reducing to a boolean, we are able to prove that the length of the standard reduction is at most a mere factorial of the length of the shortest reduction sequence. The methodological innovation of our approach is that instead of counting the cost for producing something, as is customary, we count the cost of consuming things. The key observation is that the part of a λ-term that is needed to produce the normal form (or an arbitrary rigid prefix) may rapidly augment along a computation, but can only decrease very slowly (actually, linearly).

N. G. de Bruijn, now professor emeritus of the Eindhoven University of Technology, was a pioneer in the field of interactive theorem proving. From 1967 to the end of the 1970's, his work on the Automath system introduced the architecture that is common to most of today's proof assistants, and much of the basic technology. But de Bruijn was a mathematician first and foremost, as evidenced by the many mathematical notions and results that bear his name, among them de Bruijn sequences, de Bruijn graphs, the de Bruijn–Newman constant, and the de Bruijn–Erdös theorem. The quotation above is thus interesting not because it is a reflection on his expertise in formal verification, but, rather, of his convictions as a working mathematician.

We add mobility to Place-Transition Petri nets: tokens are names for places, and an input token of a transition can be used in its postset to specify a destination. Mobile Petri nets are then further extended to dynamic nets by adding the possibility of creating new nets during the firing of a transition. In this way, starting from Petri nets, we define a simple hierarchy of nets with increasing degrees of dynamicity. For each class in this hierarchy, we provide its encoding in the former class. Our work was largely inspired by the join-calculus of Fournet and Gonthier, which turns out to be a (well-motivated) particular case of dynamic Petri nets. The main difference is that, in the preset of a transition, we allow both non-linear patterns (name unification) and (locally) free names for input places (that is, we remove the locality constraint, and preserve reflexion).

In a controversial paper (De Millo et al. 1979) at the end of the 1970's, R. A. De Millo, R. J. Lipton and A. J. Perlis argued against formal verifications of programs, mostly motivating their position by an analogy with proofs in mathematics, and, in particular, with the impracticality of a strictly formalist approach to this discipline. The recent, impressive achievements in the field of interactive theorem proving provide an interesting ground for a critical revisiting of their theses. We believe that the social nature of proof and program development is uncontroversial and ineluctable, but formal verification is not antithetical to it. Formal verification should strive not only to cope with, but to ease and enhance the collaborative, organic nature of this process, eventually helping us to master the growing complexity of scientific knowledge.

The proofs of major results of Computability Theory like Rice, Rice-Shapiro or Kleene's fixed point theorem hidemore information of what is usually expressed in theirrespective statements. We make this information explicit, allowing to state stronger, complexity theoretic-versions of all these theorems. In particular, we replace the notion of extensional set of indices of programs, by a set of indices of programs having not only the same extensional behavior but also similar complexity (Complexity Clique). We prove, under very weak complexity assumptions, that any recursive Complexity Clique is trivial, and any r.e. Complexity Clique is an extensional set (and thus satisfies Rice-Shapiro conditions). This allows, for instance, to use Rice's argument to prove that the property of having polynomial complexity is not decidable, and to use Rice-Shapiro to conclude that it is not even semi-decidable. We conclude the paper with a discussion of "complexity-theoretic" versions of Kleene's Fixed Point Theorem.

This article is a structured introduction to Intuitionistic Light Affine Logic ( ILAL ). ILAL has a polynomially costing normalization, and it is expressive enough to encode, and simulate, all PolyTime Turing machines. The bound on the normalization cost is proved by introducing the proof-nets for ILAL . The bound follows from a suitable normalization strategy that exploits structural properties of the proof-nets. This allows us to have a good understanding of the meaning of the § modality, which is a peculiarity of light logics. The expressive power of ILAL is demonstrated in full detail. Such a proof gives a hint of the nontrivial task of programming with resource limitations, using ILAL derivations as programs.

In 1998 Asperti and Mairson proved that the cost of reducing a lambda-term using an optimal lambda-reducer (a la Lévy) cannot be bound by any elementary function in the number of shared-beta steps. We prove in this paper that an analogous result holds for Lamping’s abstract algorithm. That is, there is no elementary function in the number of shared beta steps bounding the number of duplication steps of the optimal reducer. This theorem vindicates the oracle of Lamping’s algorithm as the culprit for the negative result of Asperti and Mairson. The result is obtained using as a technical tool Elementary Affine Logic. Key words: complexity, elementary affine logic, graph rewriting, optimal reduction

Much effort has been recently devoted to the study of polytime formal (and especially logical) systems. The purpose of such systems is manyfold. On the theoretical side, they provide a better understanding of what is the logical essence of polytime reduction (and other complexity classes). On the practical side, via the well known Curry-Howard correspondence, they yield sophisticated typing systems, where types provide (statically) an accurate upper bound on the complexity of the computation. Even more, the type annotations give essential information on the "efficient way" to reduce the term. The most promising of these logical systems is Girard's light linear logic. In this paper, we introduce a slight variation of LLL, by adding full weakening (for this reason, we call it light affine logic). This modification does not alter the good complexity properties of LLL: cut-elimination is still polytime. On the other side, the logical system is much simpler: we reduce it from 21 to just 11 rules, and with simpler, traditional sequents. Rephrasing Girard, we could thus say that the abuse of contraction may have damaging complexity effects, but the abstinence from weakening leads to inessential syntactical complications.

We analyze the inherent complexity of implementing Lévy's notion of optimal evaluation for the &lambda-calculus, where similar redexes are contracted in one step via so-called parallel β-reduction. optimal evaluation was finally realized by Lamping, who introduced a beautiful graph reduction technology for sharing evaluation contexts dual to the sharing of values. His pioneering insights have been modified and improved in subsequent implementations of optimal reduction.We prove that the cost of parallel β-reduction is not bounded by any Kalmár-elementary recursive function. Not merely do we establish that the parallel β-step cannot, be a unit-cost operation, we demonstrate that the time complexity of implementing a sequence of n parallel β-steps is not bounded as O(2n), O(22n), O(222n), or in general, O(Kl(n)) where Kl(n) is a fixed stack of l 2s with an n on top.A key insight, essential to the establishment of this nonelementary lower bound, is that any simply-typed λ-term can be reduced to normal form in a number of parallel β-steps that is only polynomial in the length of the explicitly-typed term. The result follows from Statman's theorem that deciding equivalence of typed λ-terms is not elementary recursive.The main theorem gives a lower bound on the work that must be done by any technology that implements Lévy's notion of optimal reduction. However, in the significant case of Lamping's solution, we make some important remarks addressing how work done by β-reduction is translated into equivalent work carried out by his bookkeeping nodes. In particular, we identify the computational paradigms of superposition of values and of higher-order sharing, appealing to compelling analogies with quantum mechanics and SIMD-parallelism.

Abstract A Partial Combinatory Algebra is completable if it can be extended to a total one. In [1] it is asked (question 11, posed by D. Scott, H. Barendregt, and G. Mitschke) if every PCA can be completed. A negative answer to this question was given by Klop in [12, 11]; moreover he provided a sufficient condition for completability of a PCA (M, •, K,S) in the form of ten axioms (inequalities) on terms of M. We prove that just one of these axiom (the so called Barendregt's axiom) is sufficient to guarantee (a slightly weaker notion of) completability.

We prove that the complexity of Lamping's optimal graph reduction technique for the λ-calculus can be exponential in the number of Lévy's family reductions. Starting from this consideration, we propose a new measure for what could be considered as "the intrinsic complexity" of λ-terms.

Abstract The Bologna Optimal Higher-order Machine (BOHM) is a prototype implementation of the core of a functional language based on (a variant of) Lamping's optimal graph reduction technique (Lamping, 1990; Gonthier et al. , 1992a; Asperti, 1994). The source language is a sugared λ-calculus enriched with booleans, integers, lists and basic operations on these data types (following the guidelines of Interaction Systems – Asperti and Laneve (1993b, 1994), Laneve (1993)). In this paper, we shall describe BOHM's general architecture (comprising the garbage collector), and give a large set of benchmarks and experimental results.

The paper discusses, in a categorical perspective, some recent works on optimal graph reduction techniques for the λ-calculus. In particular, we relate the two “brackets” in [GAL92a] to the two operations associated with the comonad “!” of Linear Log

A new correctness criterion for discriminating Proof Nets among Proof Structures of Multiplicative Linear Logic with the MIX rule is provided. This criterion is inspired by an original interpretation of Proof Structures as distributed systems, and logical formulae as processes. The computation inside a system corresponds to the logical flow of information inside a proof, that is, roughly speaking, a distributed version of Girard's token trip. Proof Nets are then characterised as deadlock free Proof Structures (deadlock free distributed systems). This result follows by explicitly considering the causal dependencies among logical formulae inside proofs, and it provides a new understanding of notions such as acyclicity, chains and empires in terms of concurrent computations.

Since the rebirth of /spl lambda/-calculus in the late 1960s, three major theoretical investigations of /spl beta/-reduction have been undertaken: (1) Levy's (1978) analysis of families of redexes (and the associated concept of labeled reductions); (2) Lamping's (1990) graph-reduction algorithm; and (3) Girard's (1988) geometry of interaction. All three studies happened to make crucial (if not always explicit) use of the notion of a path, namely and respectively: legal paths, consistent paths and regular paths. We prove that these are equivalent to each other.>

We introduce a new class of higher order rewriting systems, called Interaction Systems (IS's). IS's are derived from Lafont's (Intuitionistic) Interaction Nets (Lafont 1990) by dropping the linearity constraint. In particular, we borrow from Interaction Nets the syntactical bipartitions of operators into constructors and destructors and the principle of binary interaction. As a consequence, IS's are a subclass of Klop's Combinatory Reduction Systems (Klop 1980), where the Curry-Howard analogy still ‘makes sense’. Destructors and constructors, respectively, correspond to left and right logical introduction rules: interaction is cut and reduction is cut-elimination. Interaction Systems have been primarily motivated by the necessity of extending the practice of optimal evaluators for λ-calculus (Lamping 1990; Gonthier et al. 1992a) to other computational constructs such as conditionals and recursion. In this paper we focus on the theoretical aspects of optimal reductions. In particular, we generalize the family relation in Lévy (1978; 1980), thus defining the amount of sharing an optimal evaluator is required to perform. We reinforce our notion of family by approaching it in two different ways (generalizing labelling and extraction in Levy (1980)) and proving their coincidence. The reader is referred to Asperti and Laneve (1993c) for the paradigmatic description of optimal evaluators of IS's.

Abstract In the last two decades, category theory has become one of the main tools for the denotational investigation of programming languages. Taking advantage of the algebraic nature of the categorical semantics, and of the rewriting systems it suggests, it is possible to use these denotational descriptions as a base for research into more operational aspects of programming languages. This approach proves to be particularly interesting in the study and the definition of environment machines for functional languages. The reason is that category theory offers a simple and uniform language for handling terms and environments (substitutions), and for studying their interaction (through application). Several examples of known machines are discussed, among which the Categorical Abstract Machine of Cousineau et al. (1987) and Krivine's machine. Moreover, as an example of the power and fruitfulness of this approach, we define two original categorical machines. The first one is a variant of the CAM implementing a λ-calculus with both call-by-value and call-by-name as parameters passing modes. The second one is a variant of Krivine's machine performing complete reduction of λ-terms.

In [As87] a correspondence between the subset of Linear Logic [Gi86] involving the conjunctive tensor product only and Place/Transition Petri Nets [Rei85] is established. In this correspondence, formulae are regarded as distributed states and provable sequents are computations in the net. Developing this idea, Martì-Oliet and Meseguer [MaM89] have suggested that all the other computations of Linear Logic, which do not have an immediate correspondence with Petri Nets, should be regarded as “gedanken” or idealized processes, providing a richer language for the specification and the study of properties of distributed computations. In this paper we apply this program to the fundamental connective of linear implication. We prove that the introduction of linear implication allows us to observe the net at a lower, more decentralized level of atomicity, where the preemption of each resource needed for the firing of a transition is represented as a separate move. We give a conservative theorem relating computations at different levels of abstraction. The categorical semantics establishes a tight correspondence among Petri nets, monoidal closed categories and tensor theories, reminiscent of the well known relation among functional languages, Cartesian closed categories and intuitionistic logic [LS86]. The identification of computations in the categorical model naturally suggests the generalisation of the notion of process [DMM89] at the lower level of atomicity.