SearcharxivSearch

arXiv subjects

Fritz Müller

Publications and source records attributed to Fritz Müller.

5 recordsLinked to original sources

An overview of stray light findings and interpretation during on-sky commissioning of LSSTCam

Wide-field telescopes are intrinsically difficult to shield from unwanted stray and scattered light, while the search to identify sources of contaminating light is frequently a challenging task. The Vera C.~Rubin Observatory, which achieved its first photon with the LSST Camera (LSSTCam) on April 15, 2025, will initiate a revolutionary era for the study of dark matter, dark energy, the transient sky, the Solar System, and the Milky Way. LSSTCam will provide near seeing-limited images of the sky in six bands ($u,g,r,i,z,y$) over a $3.^\circ 5$-diameter field of view, and over the course of a decade, it will execute the Legacy Survey of Space and Time (LSST). This work provides an overview of the dedicated stray and scattered light test campaign that has been undertaken since the start of Rubin commissioning. In particular, we highlight the processes used to characterize, model, and mitigate stray light present in LSSTCam images. The Rubin commissioning team created a series of testing and analysis tools to track stray light artifacts from their initial discovery through reproduction with timely observations, simulation using ray tracing to identify opto-mechanical origins, and finally devising corrective actions. The complex stray light features encountered by Rubin provide a wealth of experience for the future wide-field and extremely wide-field observatories. This work covers the many stages of a long journey that started with conceiving an innovative and challenging optical design, followed by the engineering and system engineering efforts to build it, to finally delivering an optimized and revolutionary cutting-edge facility.

astro-ph.IM

Intensional Constructed Numbers: Towards Formalizing the Notion of Algorithm

This work is meant to be a step towards the formal definition of the notion of algorithm, in the sense of an equivalence class of programs working "in a similar way". But instead of defining equivalence transformations directly on programs, we look at the computation for each particular argument and give it a structure. This leads to the notion of constructed number: the result of the computation is a constructed number whose constructors (0, successor) carry a history condition (or trace) of their computation. There are equivalence relations on these conditions and on constructed numbers. Two programs are equivalent if they produce equivalent constructed numbers for each argument.

cs.LO

From Sazonov's Non-Dcpo Natural Domains to Closed Directed-Lub Partial Orders

Normann proved that the domains of the game model of PCF (the domains of sequential functionals) need not be dcpos. Sazonov has defined natural domains for a theory of such incomplete domains. This paper further develops that theory. It defines lub-rules that infer natural lubs from existing natural lubs, and lub-rule classes that describe axiom systems like that of natural domains. There is a canonical proper subcategory of the natural domains, the closed directed lub partial orders (cdlubpo), that corresponds to the complete lub-rule class of all valid lub-rules. Cdlubpos can be completed to restricted dcpos, which are dcpos that retain the data of the incomplete cdlubpo as a subset.

cs.LO

On Berry's conjectures about the stable order in PCF

PCF is a sequential simply typed lambda calculus language. There is a unique order-extensional fully abstract cpo model of PCF, built up from equivalence classes of terms. In 1979, Gérard Berry defined the stable order in this model and proved that the extensional and the stable order together form a bicpo. He made the following two conjectures: 1) "Extensional and stable order form not only a bicpo, but a bidomain." We refute this conjecture by showing that the stable order is not bounded complete, already for finitary PCF of second-order types. 2) "The stable order of the model has the syntactic order as its image: If a is less than b in the stable order of the model, for finite a and b, then there are normal form terms A and B with the semantics a, resp. b, such that A is less than B in the syntactic order." We give counter-examples to this conjecture, again in finitary PCF of second-order types, and also refute an improved conjecture: There seems to be no simple syntactic characterization of the stable order. But we show that Berry's conjecture is true for unary PCF. For the preliminaries, we explain the basic fully abstract semantics of PCF in the general setting of (not-necessarily complete) partial order models (f-models.) And we restrict the syntax to "game terms", with a graphical representation.

cs.LO

Full Abstraction for a Recursively Typed Lambda Calculus with Parallel Conditional

We define the syntax and reduction relation of a recursively typed lambda calculus with a parallel case-function (a parallel conditional). The reduction is shown to be confluent. We interpret the recursive types as information systems in a restricted form, which we call prime systems. A denotational semantics is defined with this interpretation. We define the syntactical normal form approximations of a term and prove the Approximation Theorem: The semantics of a term equals the limit of the semantics of its approximations. The proof uses inclusive predicates (logical relations). The semantics is adequate with respect to the observation of Boolean values. It is also fully abstract in the presence of the parallel case-function.

cs.LO