arXiv subjects

Andrew Polonsky

Publications and source records attributed to Andrew Polonsky.

14 recordsLinked to original sources

arXiv2026

A Formalization of Abstract Rewriting in Agda

We present a constructive formalization of Abstract Rewriting Systems (ARS) in the Agda proof assistant, focusing on standard results in term rewriting. We define a taxonomy of concepts related to termination and confluence and investigate the relationships between them and their classical counterparts. We identify, and eliminate where possible, the use of classical logic in the proofs of standard ARS results. Our analysis leads to refinements and mild generalizations of classical termination and confluence criteria. We investigate logical relationships between several notions of termination, arising from different formulations of the concept of a well-founded relation. We illustrate general applicability of our ARS development with an example formalization of the lambda calculus.

cs.LO↗

arXiv2024

ThermoPore: Predicting Part Porosity Based on Thermal Images Using Deep Learning

We present a deep learning approach for quantifying and localizing ex-situ porosity within Laser Powder Bed Fusion fabricated samples utilizing in-situ thermal image monitoring data. Our goal is to build the real time porosity map of parts based on thermal images acquired during the build. The quantification task builds upon the established Convolutional Neural Network model architecture to predict pore count and the localization task leverages the spatial and temporal attention mechanisms of the novel Video Vision Transformer model to indicate areas of expected porosity. Our model for porosity quantification achieved a $R^2$ score of 0.57 and our model for porosity localization produced an average IoU score of 0.32 and a maximum of 1.0. This work is setting the foundations of part porosity "Digital Twins" based on additive manufacturing monitoring data and can be applied downstream to reduce time-intensive post-inspection and testing activities during part qualification and certification. In addition, we seek to accelerate the acquisition of crucial insights normally only available through ex-situ part evaluation by means of machine learning analysis of in-situ process monitoring data.

cs.CV↗

arXiv2022

On sets of terms having a given intersection type

Working in a variant of the intersection type assignment system of Coppo, Dezani-Ciancaglini and Venneri [1981], we prove several facts about sets of terms having a given intersection type. Our main result is that every strongly normalizing term M admits a *uniqueness typing*, which is a pair $(Γ,A)$ such that 1) $Γ\vdash M : A$ 2) $Γ\vdash N : A \Longrightarrow M =_{βη} N$ We also discuss several presentations of intersection type algebras, and the corresponding choices of type assignment rules. Moreover, we show that the set of closed terms with a given type is uniformly separable, and, if infinite, forms an adequate numeral system. The proof of this fact uses an internal version of the Böhm-out technique, adapted to terms of a given intersection type.

cs.LO↗

arXiv2021

Uniqueness typing for intersection types

Working in a variant of the intersection type assignment system of Coppo, Dezani-Ciancaglini and Veneri [1981], we prove several facts about sets of terms having a given intersection type. Our main result is that every strongly normalizing term $M$ admits a *uniqueness typing*, which is a pair $(Γ,A)$ such that 1) $Γ\vdash M : A$ 2) $Γ\vdash N : A \Longrightarrow M =_{βη} N$ We also discuss several presentations of intersection type algebras, and the corresponding choices of type assignment rules.

cs.LO↗

arXiv2020

Fixed point combinators as fixed points of higher-order fixed point generators

Corrado Böhm once observed that if $Y$ is any fixed point combinator (fpc), then $Y(λyx.x(yx))$ is again fpc. He thus discovered the first "fpc generating scheme" -- a generic way to build new fpcs from old. Continuing this idea, define an $\textit{fpc generator}$ to be any sequence of terms $G_1,\dots,G_n$ such that \[ Y \in FPC \Rightarrow Y G_1 \cdots G_n \in FPC \] In this contribution, we take first steps in studying the structure of (weak) fpc generators. We isolate several robust classes of such generators, by examining their elementary properties like injectivity and (weak) constancy. We provide sufficient conditions for existence of fixed points of a given generator $(G_1,\cdots,G_n)$: an fpc $Y$ such that $Y = Y G_1 \cdots G_n$. We conjecture that weak constancy is a necessary condition for existence of such (higher-order) fixed points. This statement generalizes Statman's conjecture on non-existence of "double fpcs": fixed points of the generator $(G) = (λyx.x(yx))$ discovered by Böhm. Finally, we define and make a few observations about the monoid of (weak) fpc generators. This enables us to formulate new a conjecture about their structure.

cs.LO↗

arXiv2019

Degrees of extensionality in the theory of Böhm trees and Sallé's conjecture

The main observational equivalences of the untyped lambda-calculus have been characterized in terms of extensional equalities between Böhm trees. It is well known that the lambda-theory H*, arising by taking as observables the head normal forms, equates two lambda-terms whenever their Böhm trees are equal up to countably many possibly infinite eta-expansions. Similarly, two lambda-terms are equal in Morris's original observational theory H+, generated by considering as observable the beta-normal forms, whenever their Böhm trees are equal up to countably many finite eta-expansions. The lambda-calculus also possesses a strong notion of extensionality called "the omega-rule", which has been the subject of many investigations. It is a longstanding open problem whether the equivalence B-omega obtained by closing the theory of Böhm trees under the omega-rule is strictly included in H+, as conjectured by Sallé in the seventies. In this paper we demonstrate that the two aforementioned theories actually coincide, thus disproving Sallé's conjecture. The proof technique we develop for proving the latter inclusion is general enough to provide as a byproduct a new characterization, based on bounded eta-expansions, of the least extensional equality between Böhm trees. Together, these results provide a taxonomy of the different degrees of extensionality in the theory of Böhm trees.

cs.LO↗

arXiv2018

On local presentability of T/A

We prove that if $\mathcal{A}$ is a locally $λ$-presentable category and $T : \mathcal{A} \to \mathcal{A}$ is a $λ$-accessible functor then $T/\mathcal{A}$ is locally $λ$-presentable.

math.CT↗

arXiv2018

Coinductive Foundations of Infinitary Rewriting and Infinitary Equational Logic

We present a coinductive framework for defining and reasoning about the infinitary analogues of equational logic and term rewriting in a uniform, coinductive way. The setup captures rewrite sequences of arbitrary ordinal length, but it has neither the need for ordinals nor for metric convergence. This makes the framework especially suitable for formalizations in theorem provers.

cs.LO↗

arXiv2015

A Coinductive Framework for Infinitary Rewriting and Equational Reasoning (Extended Version)

We present a coinductive framework for defining infinitary analogues of equational reasoning and rewriting in a uniform way. We define the relation =^infty, notion of infinitary equational reasoning, and ->^infty, the standard notion of infinitary rewriting as follows: =^infty := nu R. ( <-_root + ->_root + lift(R) )^* ->^infty := mu R. nu S. ( ->_root + lift(R) )^* ; lift(S) where lift(R) := { (f(s_1,...,s_n), f(t_1,...,t_n)) | s_1 R t_1,...,s_n R t_n } + id , and where mu is the least fixed point operator and nu is the greatest fixed point operator. The setup captures rewrite sequences of arbitrary ordinal length, but it has neither the need for ordinals nor for metric convergence. This makes the framework especially suitable for formalizations in theorem provers.

cs.LO↗

arXiv2015

Internalization of extensional equality

We give a type system in which the universe of types is closed by reflection into it of the logical relation defined externally by induction on the structure of types. This contribution is placed in the context of the search for a natural, syntactic construction of the extensional equality type (Tait [1995], Altenkirch [1999], Coquand [2011], Licata and Harper [2012], Martin-Lof [2013]). The system is presented as an extension of lambda-*, the terminal pure type system in which the universe of all types is a type. The universe inconsistency is then removed by the usual method of stratification into levels. We give a set-theoretic model for the stratified system. We conjecture that Strong Normalization holds as well.

cs.LO↗

arXiv2014

An Introduction to the Clocked Lambda Calculus

We give a brief introduction to the clocked lambda calculus, an extension of the classical lambda calculus with a unary symbol tau used to witness the beta-steps. In contrast to the classical lambda calculus, this extension is infinitary strongly normalising and infinitary confluent. The infinitary normal forms are enriched Boehm Trees, which we call clocked Boehm Trees.

cs.LO↗

arXiv2014

Discriminating Lambda-Terms Using Clocked Boehm Trees

As observed by Intrigila, there are hardly techniques available in the lambda-calculus to prove that two lambda-terms are not beta-convertible. Techniques employing the usual Boehm Trees are inadequate when we deal with terms having the same Boehm Tree (BT). This is the case in particular for fixed point combinators, as they all have the same BT. Another interesting equation, whose consideration was suggested by Scott, is BY = BYS, an equation valid in the classical model P-omega of lambda-calculus, and hence valid with respect to BT-equality but nevertheless the terms are beta-inconvertible. To prove such beta-inconvertibilities, we employ `clocked' BT's, with annotations that convey information of the tempo in which the data in the BT are produced. Boehm Trees are thus enriched with an intrinsic clock behaviour, leading to a refined discrimination method for lambda-terms. The corresponding equality is strictly intermediate between beta-convertibility and Boehm Tree equality, the equality in the model P-omega. An analogous approach pertains to Levy-Longo and Berarducci Trees. Our refined Boehm Trees find in particular an application in beta-discriminating fixed point combinators (fpc's). It turns out that Scott's equation BY = BYS is the key to unlocking a plethora of fpc's, generated by a variety of production schemes of which the simplest was found by Boehm, stating that new fpc's are obtained by postfixing the term SI, also known as Smullyan's Owl. We prove that all these newly generated fpc's are indeed new, by considering their clocked BT's. Even so, not all pairs of new fpc's can be discriminated this way. For that purpose we increase the discrimination power by a precision of the clock notion that we call `atomic clock'.

cs.LO↗

arXiv2014

A Coinductive Treatment of Infinitary Rewriting

We introduce a coinductive definition of infinitary term rewriting. The setup is surprisingly simple, and has in contrast to the usual definitions of infinitary rewriting, neither need for ordinals nor for metric convergence. While the idea of a coinductive treatment of infinitary rewriting is not new, all previous approaches were limited to reductions of length at most omega. The approach presented in this paper is the first to capture the full infinitary term rewriting with reductions of arbitrary ordinal length. Apart from an elegant reformulation of known concepts, our approach gives rise, in a very natural way, to a novel notion of infinitary equational reasoning.

cs.LO↗

arXiv2014

Extensionality of lambda-*

We prove an extensionality theorem for the "type-in-type" dependent type theory with Sigma-types. We suggest that the extensional equality type be identified with the logical equivalence relation on the free term model of type theory.

cs.LO↗