-
Profinite trees, through monads and the lambda-calculus
Authors:
Vincent Moreau
Abstract:
In its simplest form, the theory of regular languages is the study of sets of finite words recognized by finite monoids. The finiteness condition on monoids gives rise to a topological space whose points, called profinite words, encode the limiting behavior of words with respect to finite monoids. Yet, some aspects of the theory of regular languages are not particular to monoids and can be describ…
▽ More
In its simplest form, the theory of regular languages is the study of sets of finite words recognized by finite monoids. The finiteness condition on monoids gives rise to a topological space whose points, called profinite words, encode the limiting behavior of words with respect to finite monoids. Yet, some aspects of the theory of regular languages are not particular to monoids and can be described in a general setting. On the one hand, Bojańczyk has shown how to use monads to generalize the theory of regular languages and has given an abstract definition of the free profinite structure, defined by codensity, given a fixed monad and a notion of finite structure. On the other hand, Salvati has introduced the notion of language of $λ$-terms, using denotational semantics, which generalizes the case of words and trees through the Church encoding. In recent work, the author and collaborators defined the notion of profinite $λ$-term using semantics in finite sets and functions, which extend the Church encoding to profinite words.
In this article, we prove that these two generalizations, based on monads and denotational semantics, coincide in the case of trees. To do so, we consider the monad of abstract clones which, when applied to a ranked alphabet, gives the associated clone of ranked trees. This induces a notion of free profinite clone, and hence of profinite trees. The main contribution is a categorical proof that the free profinite clone on a ranked alphabet is isomorphic, as a Stone-enriched clone, to the clone of profinite $λ$-terms of Church type. Moreover, we also prove a parametricity theorem on families of semantic elements which provides another equivalent formulation of profinite trees in terms of Reynolds parametricity.
△ Less
Submitted 20 February, 2024;
originally announced February 2024.
-
Syntactically and semantically regular languages of lambda-terms coincide through logical relations
Authors:
Vincent Moreau,
Lê Thành Dũng Nguyên
Abstract:
A fundamental theme in automata theory is regular languages of words and trees, and their many equivalent definitions. Salvati has proposed a generalization to regular languages of simply typed $λ$-terms, defined using denotational semantics in finite sets.
We provide here some evidence for its robustness. First, we give an equivalent syntactic characterization that naturally extends the seminal…
▽ More
A fundamental theme in automata theory is regular languages of words and trees, and their many equivalent definitions. Salvati has proposed a generalization to regular languages of simply typed $λ$-terms, defined using denotational semantics in finite sets.
We provide here some evidence for its robustness. First, we give an equivalent syntactic characterization that naturally extends the seminal work of Hillebrand and Kanellakis connecting regular languages of words and syntactic $λ$-definability. Second, we show that any finitary extensional model of the simply typed $λ$-calculus, when used in Salvati's definition, recognizes exactly the same class of languages of $λ$-terms as the category of finite sets does.
The proofs of these two results rely on logical relations and can be seen as instances of a more general construction of a categorical nature, inspired by previous categorical accounts of logical relations using the gluing construction.
△ Less
Submitted 8 February, 2024; v1 submitted 31 July, 2023;
originally announced August 2023.
-
Profinite lambda-terms and parametricity
Authors:
Sam van Gool,
Paul-André Melliès,
Vincent Moreau
Abstract:
Combining ideas coming from Stone duality and Reynolds parametricity, we formulate in a clean and principled way a notion of profinite lambda-term which, we show, generalizes at every type the traditional notion of profinite word coming from automata theory. We start by defining the Stone space of profinite lambda-terms as a projective limit of finite sets of usual lambda-terms, considered modulo…
▽ More
Combining ideas coming from Stone duality and Reynolds parametricity, we formulate in a clean and principled way a notion of profinite lambda-term which, we show, generalizes at every type the traditional notion of profinite word coming from automata theory. We start by defining the Stone space of profinite lambda-terms as a projective limit of finite sets of usual lambda-terms, considered modulo a notion of equivalence based on the finite standard model. One main contribution of the paper is to establish that, somewhat surprisingly, the resulting notion of profinite lambda-term coming from Stone duality lives in perfect harmony with the principles of Reynolds parametricity. In addition, we show that the notion of profinite lambda-term is compositional by constructing a cartesian closed category of profinite lambda-terms, and we establish that the embedding from lambda-terms modulo beta-eta-conversion to profinite lambda-terms is faithful using Statman's finite completeness theorem. Finally, we prove that the traditional Church encoding of finite words into lambda-terms can be extended to profinite words, and leads to a homeomorphism between the space of profinite words and the space of profinite lambda-terms of the corresponding Church type.
△ Less
Submitted 18 November, 2023; v1 submitted 29 January, 2023;
originally announced January 2023.
-
Ariel: Enabling planetary science across light-years
Authors:
Giovanna Tinetti,
Paul Eccleston,
Carole Haswell,
Pierre-Olivier Lagage,
Jérémy Leconte,
Theresa Lüftinger,
Giusi Micela,
Michel Min,
Göran Pilbratt,
Ludovic Puig,
Mark Swain,
Leonardo Testi,
Diego Turrini,
Bart Vandenbussche,
Maria Rosa Zapatero Osorio,
Anna Aret,
Jean-Philippe Beaulieu,
Lars Buchhave,
Martin Ferus,
Matt Griffin,
Manuel Guedel,
Paul Hartogh,
Pedro Machado,
Giuseppe Malaguti,
Enric Pallé
, et al. (293 additional authors not shown)
Abstract:
Ariel, the Atmospheric Remote-sensing Infrared Exoplanet Large-survey, was adopted as the fourth medium-class mission in ESA's Cosmic Vision programme to be launched in 2029. During its 4-year mission, Ariel will study what exoplanets are made of, how they formed and how they evolve, by surveying a diverse sample of about 1000 extrasolar planets, simultaneously in visible and infrared wavelengths.…
▽ More
Ariel, the Atmospheric Remote-sensing Infrared Exoplanet Large-survey, was adopted as the fourth medium-class mission in ESA's Cosmic Vision programme to be launched in 2029. During its 4-year mission, Ariel will study what exoplanets are made of, how they formed and how they evolve, by surveying a diverse sample of about 1000 extrasolar planets, simultaneously in visible and infrared wavelengths. It is the first mission dedicated to measuring the chemical composition and thermal structures of hundreds of transiting exoplanets, enabling planetary science far beyond the boundaries of the Solar System. The payload consists of an off-axis Cassegrain telescope (primary mirror 1100 mm x 730 mm ellipse) and two separate instruments (FGS and AIRS) covering simultaneously 0.5-7.8 micron spectral range. The satellite is best placed into an L2 orbit to maximise the thermal stability and the field of regard. The payload module is passively cooled via a series of V-Groove radiators; the detectors for the AIRS are the only items that require active cooling via an active Ne JT cooler. The Ariel payload is developed by a consortium of more than 50 institutes from 16 ESA countries, which include the UK, France, Italy, Belgium, Poland, Spain, Austria, Denmark, Ireland, Portugal, Czech Republic, Hungary, the Netherlands, Sweden, Norway, Estonia, and a NASA contribution.
△ Less
Submitted 10 April, 2021;
originally announced April 2021.
-
The Mid-Infrared Instrument for the James Webb Space Telescope, III: MIRIM, The MIRI Imager
Authors:
P. Bouchet,
M. Garcia-Marin,
P. -O. Lagage,
J. Amiaux,
J. -L. Augueres,
E. Bauwens,
J. A. D. L. Blommaert,
C. H. Chen,
O. H. Detre,
D. Dicken,
D. Dubreuil,
Ph. Galdemard,
R. Gastaud,
A. Glasse,
K. D. Gordon,
F. Gougnaud,
P. Guillard,
K. Justtanont,
O. Krause,
D. Leboeuf,
Y. Longval,
L. Martin,
E. Mazy,
V. Moreau,
G. Olofsson
, et al. (12 additional authors not shown)
Abstract:
In this article, we describe the MIRI Imager module (MIRIM), which provides broad-band imaging in the 5 - 27 microns wavelength range for the James Webb Space Telescope. The imager has a 0"11 pixel scale and a total unobstructed view of 74"x113". The remainder of its nominal 113"x113" field is occupied by the coronagraphs and the low resolution spectrometer. We present the instrument optical and m…
▽ More
In this article, we describe the MIRI Imager module (MIRIM), which provides broad-band imaging in the 5 - 27 microns wavelength range for the James Webb Space Telescope. The imager has a 0"11 pixel scale and a total unobstructed view of 74"x113". The remainder of its nominal 113"x113" field is occupied by the coronagraphs and the low resolution spectrometer. We present the instrument optical and mechanical design. We show that the test data, as measured during the test campaigns undertaken at CEA-Saclay, at the Rutherford Appleton Laboratory, and at the NASA Goddard Space Flight Center, indicate that the instrument complies with its design requirements and goals. We also discuss the operational requirements (multiple dithers and exposures) needed for optimal scientific utilization of the MIRIM.
△ Less
Submitted 11 August, 2015;
originally announced August 2015.
-
The Mid-Infrared Instrument for the James Webb Space Telescope, VIII: The MIRI Focal Plane System
Authors:
M. E. Ressler,
K. G. Sukhatme,
B. R. Franklin,
J. C. Mahoney,
M. P. Thelen,
P. Bouchet,
J. W. Colbert,
Misty Cracraft,
D. Dicken,
R. Gastaud,
G. B. Goodson,
Paul Eccleston,
V. Moreau,
G. H. Rieke,
Analyn Schneider
Abstract:
We describe the layout and unique features of the focal plane system for MIRI. We begin with the detector array and its readout integrated circuit (combining the amplifier unit cells and the multiplexer), the electronics, and the steps by which the data collection is controlled and the output signals are digitized and delivered to the JWST spacecraft electronics system. We then discuss the operati…
▽ More
We describe the layout and unique features of the focal plane system for MIRI. We begin with the detector array and its readout integrated circuit (combining the amplifier unit cells and the multiplexer), the electronics, and the steps by which the data collection is controlled and the output signals are digitized and delivered to the JWST spacecraft electronics system. We then discuss the operation of this MIRI data system, including detector readout patterns, operation of subarrays, and data formats. Finally, we summarize the performance of the system, including remaining anomalies that need to be corrected in the data pipeline.
△ Less
Submitted 10 August, 2015;
originally announced August 2015.
-
Design Differences between the Pan-STARRS PS1 and PS2 Telescopes
Authors:
Jeffrey S. Morgan,
Nicholas Kaiser,
Vincent Moreau,
David Anderson,
William Burgett
Abstract:
The PS2 telescope is the second in an array of wide-field telescopes that is being built for the Panoramic-Survey Telescope and Rapid Response System (Pan-STARRS) on Haleakala. The PS2 design has evolved incrementally based on lessons learned from PS1, but these changes should result in significant improvements in image quality, tracking performance in windy conditions, and reductions in scattered…
▽ More
The PS2 telescope is the second in an array of wide-field telescopes that is being built for the Panoramic-Survey Telescope and Rapid Response System (Pan-STARRS) on Haleakala. The PS2 design has evolved incrementally based on lessons learned from PS1, but these changes should result in significant improvements in image quality, tracking performance in windy conditions, and reductions in scattered light. The optics for this telescope are finished save for their coatings and the fabrication for the telescope structure itself is well on the way towards completion and installation on-site late this year (2012). The most significant differences between the two telescopes include the following: secondary mirror support changes, improvements in the optical polishing, changes in the optical coatings to improve throughput and decrease ghosting, removal of heat sources inside the mirror cell, expansion of the primary mirror figure control system, changes in the baffle designs, and an improved cable wrap design. This paper gives a description of each of these design changes and discusses the motivations for making them.
△ Less
Submitted 10 July, 2012;
originally announced July 2012.
-
Optical performance of the JWST MIRI flight model: characterization of the point spread function at high-resolution
Authors:
P. Guillard,
T. Rodet,
S. Ronayette,
J. Amiaux,
A. Abergel,
V. Moreau,
J. L. Augueres,
A. Bensalem,
T. Orduna,
C. Nehmé,
A. R. Belu,
E. Pantin,
P. O Lagage,
Y. Longval,
A. C. H. Glasse,
P. Bouchet,
C. Cavarroc,
D. Dubreuil,
S. Kendrew
Abstract:
The Mid Infra Red Instrument (MIRI) is one of the four instruments onboard the James Webb Space Telescope (JWST), providing imaging, coronagraphy and spectroscopy over the 5-28 microns band. To verify the optical performance of the instrument, extensive tests were performed at CEA on the flight model (FM) of the Mid-InfraRed IMager (MIRIM) at cryogenic temperatures and in the infrared. This paper…
▽ More
The Mid Infra Red Instrument (MIRI) is one of the four instruments onboard the James Webb Space Telescope (JWST), providing imaging, coronagraphy and spectroscopy over the 5-28 microns band. To verify the optical performance of the instrument, extensive tests were performed at CEA on the flight model (FM) of the Mid-InfraRed IMager (MIRIM) at cryogenic temperatures and in the infrared. This paper reports on the point spread function (PSF) measurements at 5.6 microns, the shortest operating wavelength for imaging. At 5.6 microns the PSF is not Nyquist-sampled, so we use am original technique that combines a microscanning measurement strategy with a deconvolution algorithm to obtain an over-resolved MIRIM PSF. The microscanning consists in a sub-pixel scan of a point source on the focal plane. A data inversion method is used to reconstruct PSF images that are over-resolved by a factor of 7 compared to the native resolution of MIRI. We show that the FWHM of the high-resolution PSFs were 5-10% wider than that obtained with Zemax simulations. The main cause was identified as an out-of-specification tilt of the M4 mirror. After correction, two additional test campaigns were carried out, and we show that the shape of the PSF is conform to expectations. The FWHM of the PSFs are 0.18-0.20 arcsec, in agreement with simulations. 56.1-59.2% of the total encircled energy (normalized to a 5 arcsec radius) is contained within the first dark Airy ring, over the whole field of view. At longer wavelengths (7.7-25.5 microns), this percentage is 57-68%. MIRIM is thus compliant with the optical quality requirements. This characterization of the MIRIM PSF, as well as the deconvolution method presented here, are of particular importance, not only for the verification of the optical quality and the MIRI calibration, but also for scientific applications.
△ Less
Submitted 29 June, 2010;
originally announced June 2010.
-
Design of mid-IR and THz quantum cascade laser cavities with complete TM photonic bandgap
Authors:
Michael Bahriz,
Orion Crisafulli,
Virginie Moreau,
Raffaele Colombelli,
Oskar Painter
Abstract:
We present the design of mid-infrared and THz quantum cascade laser cavities formed from planar photonic crystals with a complete in-plane photonic bandgap. The design is based on a honeycomb lattice, and achieves a full in-plane photonic gap for transverse-magnetic polarized light while preserving a connected pattern for efficient electrical injection. Candidate defects modes for lasing are ide…
▽ More
We present the design of mid-infrared and THz quantum cascade laser cavities formed from planar photonic crystals with a complete in-plane photonic bandgap. The design is based on a honeycomb lattice, and achieves a full in-plane photonic gap for transverse-magnetic polarized light while preserving a connected pattern for efficient electrical injection. Candidate defects modes for lasing are identified. This lattice is then used as a model system to demonstrate a novel effect: under certain conditions - that are typically satisfied in the THz range - a complete photonic gap can be obtained by the sole patterning of the top metal contact. This possibility greatly reduces the required fabrication complexity and avoids potential damage of the semiconductor active region.
△ Less
Submitted 11 January, 2007;
originally announced January 2007.
