-
Stellar ejection velocities from the binary supernova scenario: A comparison across population synthesis codes
Authors:
Tom Wagg,
David D. Hendriks,
Mathieu Renzo,
Katelyn Breivik
Abstract:
The vast majority of binary systems are disrupted at the moment of the first supernova, resulting in an unbound compact object and companion star. These ejected companion stars contribute to the observed population of runaway stars. Therefore, an understanding of their ejection velocities is essential to interpreting observations, particularly in the Gaia era of high-precision astronomy.
We pres…
▽ More
The vast majority of binary systems are disrupted at the moment of the first supernova, resulting in an unbound compact object and companion star. These ejected companion stars contribute to the observed population of runaway stars. Therefore, an understanding of their ejection velocities is essential to interpreting observations, particularly in the Gaia era of high-precision astronomy.
We present a comparison of the predicted ejection velocities of disrupted binary companions in three different population synthesis codes: COSMIC, COMPAS, and binary_c, which use two independent algorithms for the treatment of natal kicks. We confirm that, despite the codes producing different pre-supernova evolution from the same initial conditions, they each find the ejection velocities of secondary stars from disrupted binaries are narrowly distributed about their pre-supernova orbital velocity. We additionally include a correction to the derivation included in Kiel & Hurley 2009 that brings it into agreement with methods from other works for determining post-supernova binary orbital parameters. During this comparison, we identified and resolved bugs in the kick prescriptions of \textit{all three} codes we considered, highlighting how open-science practices and code comparisons are essential for addressing implementation issues.
△ Less
Submitted 22 April, 2025;
originally announced April 2025.
-
Honey, I Shrunk the Language Model: Impact of Knowledge Distillation Methods on Performance and Explainability
Authors:
Daniel Hendriks,
Philipp Spitzer,
Niklas Kühl,
Gerhard Satzger
Abstract:
Artificial Intelligence (AI) has increasingly influenced modern society, recently in particular through significant advancements in Large Language Models (LLMs). However, high computational and storage demands of LLMs still limit their deployment in resource-constrained environments. Knowledge distillation addresses this challenge by training a small student model from a larger teacher model. Prev…
▽ More
Artificial Intelligence (AI) has increasingly influenced modern society, recently in particular through significant advancements in Large Language Models (LLMs). However, high computational and storage demands of LLMs still limit their deployment in resource-constrained environments. Knowledge distillation addresses this challenge by training a small student model from a larger teacher model. Previous research has introduced several distillation methods for both generating training data and for training the student model. Despite their relevance, the effects of state-of-the-art distillation methods on model performance and explainability have not been thoroughly investigated and compared. In this work, we enlarge the set of available methods by applying critique-revision prompting to distillation for data generation and by synthesizing existing methods for training. For these methods, we provide a systematic comparison based on the widely used Commonsense Question-Answering (CQA) dataset. While we measure performance via student model accuracy, we employ a human-grounded study to evaluate explainability. We contribute new distillation methods and their comparison in terms of both performance and explainability. This should further advance the distillation of small language models and, thus, contribute to broader applicability and faster diffusion of LLM technology.
△ Less
Submitted 22 April, 2025;
originally announced April 2025.
-
A stellar evolutionary grid for binary population synthesis: from the main sequence to helium ignition
Authors:
Natalie R. Rees,
Robert G. Izzard,
David D. Hendriks
Abstract:
Mass changes due to strong stellar winds and binary mass transfer have a dramatic impact on the consequent evolution of stars. This is generally not accounted for in population synthesis codes which are built using single star evolution models from full stellar evolution codes. We produce a new grid of models using the 1D stellar evolution code \textit{MESA} which includes models with a range of c…
▽ More
Mass changes due to strong stellar winds and binary mass transfer have a dramatic impact on the consequent evolution of stars. This is generally not accounted for in population synthesis codes which are built using single star evolution models from full stellar evolution codes. We produce a new grid of models using the 1D stellar evolution code \textit{MESA} which includes models with a range of core mass fractions, at each total stellar mass, evolved from core hydrogen exhaustion to the onset of core helium burning. The model grid is used to produce an interpolation table, designed for use in population synthesis codes such as \textit{binary\_c}. We test the interpolation table with a simple integration algorithm to evaluate its capability of reproducing accurate evolutionary tracks. We test our method for stellar masses in the range $M=1-16~\mathrm{M}_\odot$ and show that it successfully reproduces the Hertzpsrung-gap and giant branch lifetime, the core mass at helium ignition and the HR diagram.
△ Less
Submitted 22 March, 2025;
originally announced March 2025.
-
Anomalously low-mass core-He-burning star in NGC 6819 as a post-common-envelope phase product
Authors:
Massimiliano Matteuzzi,
David Hendriks,
Robert G. Izzard,
Andrea Miglio,
Karsten Brogaard,
Josefina Montalbán,
Marco Tailo,
Alessandro Mazzi
Abstract:
Precise masses of red-giant stars enable a robust inference of their ages, but there are cases where these age estimates are highly precise yet very inaccurate. Examples are core-helium-burning (CHeB) stars that have lost more mass than predicted by standard single-star evolutionary models. Members of star clusters in the ${\it Kepler}$ database represent a unique opportunity to identify such star…
▽ More
Precise masses of red-giant stars enable a robust inference of their ages, but there are cases where these age estimates are highly precise yet very inaccurate. Examples are core-helium-burning (CHeB) stars that have lost more mass than predicted by standard single-star evolutionary models. Members of star clusters in the ${\it Kepler}$ database represent a unique opportunity to identify such stars, because they combine exquisite asteroseismic constraints with independent age information. In this work we focus on the single, metal-rich, Li-rich, low-mass, CHeB star KIC4937011, which is a member of the open cluster NGC 6819 (turn-off mass of $\approx 1.6 \, M_\odot$, i.e. age of $\approx 2.4$ Gyr). This star has $\approx 1 \, M_\odot$ less mass than expected for its age and metallicity, which could be explained by binary interactions or mass-loss along the red-giant branch (RGB). To infer formation scenarios for this object, we perform a Bayesian analysis by combining the binary stellar evolutionary framework $\texttt{binary_c v2.2.3}$ with the dynamic nested sampling approach contained in the $\texttt{dynesty v2.1.1}$ package. We find that this star is likely the result of a common-envelope evolution (CEE) phase during the RGB stage of the primary star in which the low-mass ($<0.71 \, M_\odot$) main sequence companion does not survive. During the CEE phase $\approx 1 \, M_\odot$ of material is ejected from the system, and the final star reaches the CHeB stage after helium flashes as if it were a single star of mass $\approx 0.7 \, M_\odot$, which is what we observe today. Although the proposed scenario is consistent with photometric and spectroscopic observations, a quantitative comparison with detailed stellar evolution calculations is needed to quantify the systematic skewness of radius, luminosity, and effective temperature distributions towards higher values than observations.
△ Less
Submitted 20 August, 2024;
originally announced August 2024.
-
libcdict: fast dictionaries in C
Authors:
Robert G. Izzard,
David D. Hendriks,
Daniel P. Nemergut
Abstract:
A common requirement in science is to store and share large sets of simulation data in an efficient, nested, flexible and human-readable way. Such datasets contain number counts and distributions, i.e. histograms and maps, of arbitrary dimension and variable type, e.g. floating-point number, integer or character string. Modern high-level programming languages like Perl and Python have associated a…
▽ More
A common requirement in science is to store and share large sets of simulation data in an efficient, nested, flexible and human-readable way. Such datasets contain number counts and distributions, i.e. histograms and maps, of arbitrary dimension and variable type, e.g. floating-point number, integer or character string. Modern high-level programming languages like Perl and Python have associated arrays, knowns as dictionaries or hashes, respectively, to fulfil this storage need. Low-level languages used more commonly for fast computational simulations, such as C and Fortran, lack this functionality. We present libcdict, a C dictionary library, to solve this problem. Libcdict provides C and Fortran application programming interfaces (APIs) to native dictionaries, called cdicts, and functions for cdicts to load and save these as JSON and hence for easy interpretation in other software and languages like Perl, Python and R.
△ Less
Submitted 25 January, 2024;
originally announced January 2024.
-
The impact of binary stars on the dust and metal evolution of galaxies
Authors:
Robert M. Yates,
David Hendriks,
Aswin P. Vijayan,
Robert G. Izzard,
Peter A. Thomas,
Payel Das
Abstract:
We present detailed implementations of (a) binary stellar evolution (using binary_c) and (b) dust production and destruction into the cosmological semi-analytic galaxy evolution simulation, L-Galaxies. This new version of L-Galaxies is compared to a version assuming only single stars and to global and spatially-resolved observational data across a range of redshifts ($z$). We find that binaries ha…
▽ More
We present detailed implementations of (a) binary stellar evolution (using binary_c) and (b) dust production and destruction into the cosmological semi-analytic galaxy evolution simulation, L-Galaxies. This new version of L-Galaxies is compared to a version assuming only single stars and to global and spatially-resolved observational data across a range of redshifts ($z$). We find that binaries have a negligible impact on the stellar masses, gas masses, and star formation rates of galaxies only if the total mass ejected by massive stars is unchanged. This is because massive stars determine the strength of supernova (SN) feedback, which in turn regulates galaxy growth. Binary effects, such as common envelope ejection and novae, affect carbon and nitrogen enrichment in galaxies, however heavier alpha elements are more affected by the choice of SN and wind yields. Unlike many other simulations, the new L-Galaxies reproduces observed dust-to-metal (DTM) and dust-to-gas (DTG) ratios at $z\sim{}0-4$. This is mainly due to shorter dust accretion timescales in dust-rich environments. However, dust masses are under-predicted at $z>4$, highlighting the need for enhanced dust production at early times in simulations, possibly accompanied by increased star formation. On sub-galactic scales, there is very good agreement between L-Galaxies and observed dust and metal radial profiles at $z=0$. A drop in DTM ratio is also found in diffuse, low-metallicity regions, contradicting the assumption of a universal value. We hope that this work serves as a useful template for binary stellar evolution implementations in other cosmological simulations in future.
△ Less
Submitted 23 October, 2023;
originally announced October 2023.
-
Pulsational pair-instability supernovae in gravitational-wave and electromagnetic transients
Authors:
D. D. Hendriks,
L. A. C. van Son,
M. Renzo,
R. G. Izzard,
R. Farmer
Abstract:
Current observations of binary black-hole ({BBH}) merger events show support for a feature in the primary BH-mass distribution at $\sim\,35\,\mathrm{M}_{\odot}$, previously interpreted as a signature of pulsational pair-instability (PPISN) supernovae. Such supernovae are expected to map a wide range of pre-supernova carbon-oxygen (CO) core masses to a narrow range of BH masses, producing a peak in…
▽ More
Current observations of binary black-hole ({BBH}) merger events show support for a feature in the primary BH-mass distribution at $\sim\,35\,\mathrm{M}_{\odot}$, previously interpreted as a signature of pulsational pair-instability (PPISN) supernovae. Such supernovae are expected to map a wide range of pre-supernova carbon-oxygen (CO) core masses to a narrow range of BH masses, producing a peak in the BH mass distribution. However, recent numerical simulations place the mass location of this peak above $50\,\mathrm{M}_{\odot}$. Motivated by uncertainties in the progenitor's evolution and explosion mechanism, we explore how modifying the distribution of BH masses resulting from PPISN affects the populations of gravitational-wave (GW) and electromagnetic (EM) transients. To this end, we simulate populations of isolated {BBH} systems and combine them with cosmic star-formation rates. Our results are the first cosmological BBH-merger predictions made using the \textsc{binary\_c} rapid population synthesis framework. We find that our fiducial model does not match the observed GW peak. We can only explain the $35\,\mathrm{M}_{\odot}$ peak with PPISNe by shifting the expected CO core-mass range for PPISN downwards by $\sim{}15\,\mathrm{M}_{\odot}$. Apart from being in tension with state-of-the art stellar models, we also find that this is likely in tension with the observed rate of hydrogen-less super-luminous supernovae. Conversely, shifting the mass range upward, based on recent stellar models, leads to a predicted third peak in the BH mass function at $\sim{}64\,\mathrm{M}_{\odot}$. Thus we conclude that the $\sim{}35\,\mathrm{M}_{\odot}$ feature is unlikely to be related to PPISNe.
△ Less
Submitted 17 September, 2023;
originally announced September 2023.
-
Mass-stream trajectories with non-synchronously rotating donors
Authors:
David Hendriks,
Robert Izzard
Abstract:
Mass-transfer interactions in binary stars can lead to accretion disk formation, mass loss from the system and spin-up of the accretor. To determine the trajectory of the mass-transfer stream, and whether it directly impacts the accretor, or forms an accretion disk, requires numerical simulations. The mass-transfer stream is approximately ballistic, and analytic approximations based on such trajec…
▽ More
Mass-transfer interactions in binary stars can lead to accretion disk formation, mass loss from the system and spin-up of the accretor. To determine the trajectory of the mass-transfer stream, and whether it directly impacts the accretor, or forms an accretion disk, requires numerical simulations. The mass-transfer stream is approximately ballistic, and analytic approximations based on such trajectories are used in many binary population synthesis codes as well as in detailed stellar evolution codes. We use binary population synthesis to explore the conditions under which mass transfer takes place. We then solve the reduced three-body equations to compute the trajectory of a particle in the stream for systems with varying system mass ratio, donor synchronicity and initial stream velocity. Our results show that on average both more mass and more time is spent during mass transfer from a sub-synchronous donor than from a synchronous donor. Moreover, we find that at low initial stream velocity the asynchronous rotation of the donor leads to self-accretion over a large range of mass ratios, especially for super-synchronous donors. The stream (self-)intersects in a narrow region of parameter space where it transitions between accreting onto the donor or the accretor. Increasing the initial stream velocity leads to larger areas of the parameter space where the stream accretes onto the accretor, but also more (self-)intersection. The radii of closest approach generally increase, but the range of specific angular momenta that these trajectories carry at the radius of closest approach gets broader. Our results are made publicly available.
△ Less
Submitted 1 August, 2023; v1 submitted 10 July, 2023;
originally announced July 2023.
-
Detailed equilibrium and dynamical tides: impact on circularization and synchronization in open clusters
Authors:
Giovanni M. Mirouh,
David D. Hendriks,
Sophie Dykes,
Maxwell Moe,
Robert G. Izzard
Abstract:
Binary stars evolve into chemically-peculiar objects and are a major driver of the Galactic enrichment of heavy elements. During their evolution they undergo interactions, including tides, that circularize orbits and synchronize stellar spins, impacting both individual systems and stellar populations. Using Zahn's tidal theory and MESA main-sequence model grids, we derive the governing parameters…
▽ More
Binary stars evolve into chemically-peculiar objects and are a major driver of the Galactic enrichment of heavy elements. During their evolution they undergo interactions, including tides, that circularize orbits and synchronize stellar spins, impacting both individual systems and stellar populations. Using Zahn's tidal theory and MESA main-sequence model grids, we derive the governing parameters $λ_{lm}$ and $E_2$, and implement them in the new MINT library of the stellar population code BINARY_C. Our MINT equilibrium tides are 2 to 5 times more efficient than the ubiquitous BSE prescriptions while the radiative-tide efficiency drops sharply with increasing age. We also implement precise initial distributions based on bias-corrected observations. We assess the impact of tides and initial orbital-parameter distributions on circularization and synchronization in eight open clusters, comparing synthetic populations and observations through a bootstrapping method. We find that changing the tidal prescription yields no statistically-significant improvement as both calculations typically lie within 0.5$σ$. The initial distribution, especially the primordial concentration of systems at $\log_{10}(P/{\rm d}) \approx 0.8, e\approx 0.05$ dominates the statistics even when artificially increasing tidal strength. This confirms the inefficiency of tides on the main sequence and shows that constraining tidal-efficiency parameters using the $e-\log_{10}(P/{\rm d})$ distribution alone is difficult or impossible. Orbital synchronization carries a more striking age-dependent signature of tidal interactions. In M35 we find twice as many synchronized rotators in our MINT calculation as with BSE. This measure of tidal efficiency is verifiable with combined measurements of orbital parameters and stellar spins.
△ Less
Submitted 5 July, 2023;
originally announced July 2023.
-
binary_c-python: A Python-based stellar population synthesis tool and interface to binary_c
Authors:
D. D. Hendriks,
R. G. Izzard
Abstract:
We present the software package binary_c-python which provides a convenient and easy-to-use interface to the binary_c framework, allowing the user to rapidly evolve individual systems and populations of stars. binary_c-python is available on Pip and on GitLab. binary_c-python contains many useful features to control and process the output of binary_c, like by providing binary_c-python with logging…
▽ More
We present the software package binary_c-python which provides a convenient and easy-to-use interface to the binary_c framework, allowing the user to rapidly evolve individual systems and populations of stars. binary_c-python is available on Pip and on GitLab. binary_c-python contains many useful features to control and process the output of binary_c, like by providing binary_c-python with logging statements that are dynamically compiled and loaded into binary_c. Moreover, we have recently added standardised output of events like Roche-lobe overflow or double compact-object formation to binary_c, and automatic parsing and managing of that output in binary_c-python. binary_c-python uses multiprocessing to utilise all the cores on a particular machine, and can run populations with HPC cluster workload managers like HTCondor and Slurm, allowing the user to run simulations on large computing clusters. We provide documentation that is automatically generated based on docstrings and a suite of Jupyter notebooks. These notebooks consist of technical tutorials on how to use binary_c-python and use-case scenarios aimed at doing science. Much of binary_c-python is covered by unit tests to ensure reliability and correctness, and the test coverage is continually increased as the package is improved.
△ Less
Submitted 5 June, 2023;
originally announced June 2023.
-
Population III X-ray Binaries and their Impact on the Early Universe
Authors:
Nina S. Sartorio,
A. Fialkov,
T. Hartwig,
G. M. Mirouh,
R. G. Izzard,
M. Magg,
R. S. Klessen,
S. C. O. Glover,
L. Chen,
Y. Tarumi,
D. D. Hendriks
Abstract:
The first population of X-ray binaries (XRBs) is expected to affect the thermal and ionization states of the gas in the early Universe. Although these X-ray sources are predicted to have important implications for high-redshift observable signals, such as the hydrogen 21-cm signal from cosmic dawn and the cosmic X-ray background, their properties are poorly explored, leaving theoretical models lar…
▽ More
The first population of X-ray binaries (XRBs) is expected to affect the thermal and ionization states of the gas in the early Universe. Although these X-ray sources are predicted to have important implications for high-redshift observable signals, such as the hydrogen 21-cm signal from cosmic dawn and the cosmic X-ray background, their properties are poorly explored, leaving theoretical models largely uninformed. In this paper we model a population of X-ray binaries arising from zero metallicity stars. We explore how their properties depend on the adopted initial mass function (IMF) of primordial stars, finding a strong effect on their number and X-ray production efficiency. We also present scaling relations between XRBs and their X-ray emission with the local star formation rate, which can be used in sub-grid models in numerical simulations to improve the X-ray feedback prescriptions. Specifically, we find that the uniformity and strength of the X-ray feedback in the intergalactic medium is strongly dependant on the IMF. Bottom-heavy IMFs result in a smoother distribution of XRBs, but have a luminosity orders of magnitude lower than more top-heavy IMFs. Top-heavy IMFs lead to more spatially uneven, albeit strong, X-ray emission. An intermediate IMF has a strong X-ray feedback while sustaining an even emission across the intergalactic medium. These differences in X-ray feedback could be probed in the future with measurements of the cosmic dawn 21-cm line of neutral hydrogen, which offers us a new way of constraining population III IMF.
△ Less
Submitted 6 March, 2023;
originally announced March 2023.
-
A Multi-level Methodology for Behavioral Comparison of Software-Intensive Systems
Authors:
Dennis Hendriks,
Arjan van der Meer,
Wytse Oortwijn
Abstract:
Software-intensive systems constantly evolve. To prevent software changes from unintentionally introducing costly system defects, it is important to understand their impact to reduce risk. However, it is in practice nearly impossible to foresee the full impact of software changes when dealing with huge industrial systems with many configurations and usage scenarios. To assist developers with chang…
▽ More
Software-intensive systems constantly evolve. To prevent software changes from unintentionally introducing costly system defects, it is important to understand their impact to reduce risk. However, it is in practice nearly impossible to foresee the full impact of software changes when dealing with huge industrial systems with many configurations and usage scenarios. To assist developers with change impact analysis we introduce a novel multi-level methodology for behavioral comparison of software-intensive systems. Our fully automated methodology is based on comparing state machine models of software behavior. We combine existing complementary comparison methods into a novel approach, guiding users step by step though relevant differences by gradually zooming into more and more detail. We empirically evaluate our work through a qualitative exploratory field study, showing its practical value using multiple case studies at ASML, a leading company in developing lithography systems. Our method shows great potential for preventing regressions in system behavior for software changes.
△ Less
Submitted 17 May, 2022;
originally announced May 2022.
-
Pair-instability mass loss for top-down compact object mass calculations
Authors:
M. Renzo,
D. D. Hendriks,
L. A. C. van Son,
R. Farmer
Abstract:
Population synthesis relies on semi-analytic formulae to determine masses of compact objects from the (helium or carbon-oxygen) cores of collapsing stars. Such formulae are combined across mass ranges that span different explosion mechanisms, potentially introducing artificial features in the compact object mass distribution. Such artifacts impair the interpretation of gravitational-wave observati…
▽ More
Population synthesis relies on semi-analytic formulae to determine masses of compact objects from the (helium or carbon-oxygen) cores of collapsing stars. Such formulae are combined across mass ranges that span different explosion mechanisms, potentially introducing artificial features in the compact object mass distribution. Such artifacts impair the interpretation of gravitational-wave observations. We propose a "top-down" remnant mass prescription where we remove mass from the star for each possible mass-loss mechanism, instead of relying on the fallback onto a "proto-compact-object" to get the final mass. For one of these mass-loss mechanisms, we fit the metallicity-dependent mass lost to pulsational-pair instability supernovae from numerical simulations. By imposing no mass loss in the absence of pulses, our approach recovers the existing compact object masses prescription at the low mass end and ensures continuity across the core-collapse/pulsational-pair-instability regime. Our remnant mass prescription can be extended to include other mass-loss mechanisms at the final collapse.
△ Less
Submitted 19 January, 2022;
originally announced January 2022.
-
Polluting the pair-instability mass gap for binary black holes through super-Eddington accretion in isolated binaries
Authors:
L. A. C. van Son,
S. E. de Mink,
F. S. Broekgaarden,
M. Renzo,
S. Justham,
E. Laplace,
J. Moran-Fraile,
D. D. Hendriks,
R. Farmer
Abstract:
The theory for single stellar evolution predicts a gap in the mass distribution of black holes (BHs) between approximately 45-130M$_{\odot}$, the so-called "pair-instability mass gap". We examine whether BHs can pollute the gap after accreting from a stellar companion. To this end, we simulate the evolution of isolated binaries using a population synthesis code, where we allow for super-Eddington…
▽ More
The theory for single stellar evolution predicts a gap in the mass distribution of black holes (BHs) between approximately 45-130M$_{\odot}$, the so-called "pair-instability mass gap". We examine whether BHs can pollute the gap after accreting from a stellar companion. To this end, we simulate the evolution of isolated binaries using a population synthesis code, where we allow for super-Eddington accretion. Under our most extreme assumptions, we find that at most about 2% of all merging binary BH systems contains a BH with a mass in the pair-instability mass gap, and we find that less than 0.5% of the merging systems has a total mass larger than 90M$_{\odot}$. We find no merging binary BH systems with a total mass exceeding 100M$_{\odot}$. We compare our results to predictions from several dynamical pathways to pair-instability mass gap events and discuss the distinguishable features. We conclude that the classical isolated binary formation scenario will not significantly contribute to the pollution of the pair-instability mass gap. The robustness of the predicted mass gap for the isolated binary channel is promising for the prospective of placing constraints on (i) the relative contribution of different formation channels, (ii) the physics of the progenitors including nuclear reaction rates, and (iii), tentatively, the Hubble parameter.
△ Less
Submitted 1 June, 2020; v1 submitted 10 April, 2020;
originally announced April 2020.
-
Universality of Univariate Mixed Fractions in Divisive Meadows
Authors:
Jan A. Bergstra,
Inge Bethke,
Dimitri Hendriks
Abstract:
Univariate fractions can be transformed to mixed fractions in the equational theory of meadows of characteristic zero.
Univariate fractions can be transformed to mixed fractions in the equational theory of meadows of characteristic zero.
△ Less
Submitted 3 July, 2017;
originally announced July 2017.
-
Coinductive Foundations of Infinitary Rewriting and Infinitary Equational Logic
Authors:
Jörg Endrullis,
Helle Hvid Hansen,
Dimitri Hendriks,
Andrew Polonsky,
Alexandra Silva
Abstract:
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.
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.
△ Less
Submitted 9 January, 2018; v1 submitted 31 May, 2017;
originally announced June 2017.
-
The Degree of Squares is an Atom (Extended Version)
Authors:
Jörg Endrullis,
Clemens Grabmayer,
Dimitri Hendriks,
Hans Zantema
Abstract:
We answer an open question in the theory of degrees of infinite sequences with respect to transducibility by finite-state transducers. An initial study of this partial order of degrees was carried out in (Endrullis, Hendriks, Klop, 2011), but many basic questions remain unanswered. One of the central questions concerns the existence of atom degrees, other than the degree of the `identity sequence'…
▽ More
We answer an open question in the theory of degrees of infinite sequences with respect to transducibility by finite-state transducers. An initial study of this partial order of degrees was carried out in (Endrullis, Hendriks, Klop, 2011), but many basic questions remain unanswered. One of the central questions concerns the existence of atom degrees, other than the degree of the `identity sequence' 1 0^0 1 0^1 1 0^2 1 0^3 .... A degree is called an `atom' if below it there is only the bottom degree 0, which consists of the ultimately periodic sequences. We show that also the degree of the `squares sequence' 1 0^0 1 0^1 1 0^4 1 0^9 1 0^{16} ... is an atom. As the main tool for this result we characterise the transducts of `spiralling' sequences and their degrees. We use this to show that every transduct of a `polynomial sequence' either is in 0 or can be transduced back to a polynomial sequence for a polynomial of the same order.
△ Less
Submitted 2 June, 2015;
originally announced June 2015.
-
A Coinductive Framework for Infinitary Rewriting and Equational Reasoning (Extended Version)
Authors:
Jörg Endrullis,
Helle Hvid Hansen,
Dimitri Hendriks,
Andrew Polonsky,
Alexandra Silva
Abstract:
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)…
▽ More
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.
△ Less
Submitted 5 May, 2015;
originally announced May 2015.
-
Regularity Preserving but not Reflecting Encodings
Authors:
Jörg Endrullis,
Clemens Grabmayer,
Dimitri Hendriks
Abstract:
Encodings, that is, injective functions from words to words, have been studied extensively in several settings. In computability theory the notion of encoding is crucial for defining computability on arbitrary domains, as well as for comparing the power of models of computation. In language theory much attention has been devoted to regularity preserving functions.
A natural question arising in t…
▽ More
Encodings, that is, injective functions from words to words, have been studied extensively in several settings. In computability theory the notion of encoding is crucial for defining computability on arbitrary domains, as well as for comparing the power of models of computation. In language theory much attention has been devoted to regularity preserving functions.
A natural question arising in these contexts is: Is there a bijective encoding such that its image function preserves regularity of languages, but its pre-image function does not? Our main result answers this question in the affirmative: For every countable class C of languages there exists a bijective encoding f such that for every language L in C its image f[L] is regular.
Our construction of such encodings has several noteworthy consequences. Firstly, anomalies arise when models of computation are compared with respect to a known concept of implementation that is based on encodings which are not required to be computable: Every countable decision model can be implemented, in this sense, by finite-state automata, even via bijective encodings. Hence deterministic finite-state automata would be equally powerful as Turing machine deciders.
A second consequence concerns the recognizability of sets of natural numbers via number representations and finite automata. A set of numbers is said to be recognizable with respect to a representation if an automaton accepts the language of representations. Our result entails that there is one number representation with respect to which every recursive set is recognizable.
△ Less
Submitted 20 January, 2015;
originally announced January 2015.
-
An Introduction to the Clocked Lambda Calculus
Authors:
Jörg Endrullis,
Dimitri Hendriks,
Jan Willem Klop,
Andrew Polonsky
Abstract:
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.
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.
△ Less
Submitted 29 May, 2014;
originally announced May 2014.
-
Infinitary Term Rewriting for Weakly Orthogonal Systems: Properties and Counterexamples
Authors:
Joerg Endrullis,
Clemens Grabmayer,
Dimitri Hendriks,
Jan Willem Klop,
Vincent van Oostrom
Abstract:
We present some contributions to the theory of infinitary rewriting for weakly orthogonal term rewrite systems, in which critical pairs may occur provided they are trivial. We show that the infinitary unique normal form property fails by an example of a weakly orthogonal TRS with two collapsing rules. By translating this example, we show that this property also fails for the infinitary lambda-bet…
▽ More
We present some contributions to the theory of infinitary rewriting for weakly orthogonal term rewrite systems, in which critical pairs may occur provided they are trivial. We show that the infinitary unique normal form property fails by an example of a weakly orthogonal TRS with two collapsing rules. By translating this example, we show that this property also fails for the infinitary lambda-beta-eta-calculus. As positive results we obtain the following: Infinitary confluence, and hence the infinitary unique normal forms property, holds for weakly orthogonal TRSs that do not contain collapsing rules. To this end we refine the compression lemma. Furthermore, we establish the triangle and diamond properties for infinitary multi-steps (complete developments) in weakly orthogonal TRSs, by refining an earlier cluster-analysis for the finite case.
△ Less
Submitted 5 June, 2014; v1 submitted 24 March, 2014;
originally announced March 2014.
-
A Coinductive Treatment of Infinitary Rewriting
Authors:
Joerg Endrullis,
Helle Hvid Hansen,
Dimitri Hendriks,
Andrew Polonsky,
Alexandra Silva
Abstract:
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 present…
▽ More
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.
△ Less
Submitted 10 April, 2014; v1 submitted 26 June, 2013;
originally announced June 2013.
-
Discriminating Lambda-Terms Using Clocked Boehm Trees
Authors:
Joerg Endrullis,
Dimitri Hendriks,
Jan Willem Klop,
Andrew Polonsky
Abstract:
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…
▽ More
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'.
△ Less
Submitted 22 May, 2014; v1 submitted 3 December, 2012;
originally announced December 2012.
-
On Periodically Iterated Morphisms
Authors:
Joerg Endrullis,
Dimitri Hendriks
Abstract:
We investigate the computational power of periodically iterated morphisms, also known as D0L systems with periodic control, PD0L systems for short. These systems give rise to a class of one-sided infinite sequences, called PD0L words.
We construct a PD0L word with exponential subword complexity, thereby answering a question raised by Lepisto (1993) on the existence of such words. We solve anothe…
▽ More
We investigate the computational power of periodically iterated morphisms, also known as D0L systems with periodic control, PD0L systems for short. These systems give rise to a class of one-sided infinite sequences, called PD0L words.
We construct a PD0L word with exponential subword complexity, thereby answering a question raised by Lepisto (1993) on the existence of such words. We solve another open problem concerning the decidability of the first-order theories of PD0L words; we show it is already undecidable whether a certain letter occurs in a PD0L word. This stands in sharp contrast to the situation for D0L words (purely morphic words), which are known to have at most quadratic subword complexity, and for which the monadic theory is decidable.
The main result of our paper, leading to these answers, is that every computable word w over an alphabet Sigma can be embedded in a PD0L word u over an extended alphabet Gamma in the following two ways: (i) such that every finite prefix of w is a subword of u, and (ii) such that w is obtained from u by erasing all letters from Gamma not in Sigma. The PD0L system generating such a word u is constructed by encoding a Fractran program that computes the word w; Fractran is a programming language as powerful as Turing Machines.
As a consequence of (ii), if we allow the application of finite state transducers to PD0L words, we obtain the set of all computable words. Thus the set of PD0L words is not closed under finite state transduction, whereas the set of D0L words is. It moreover follows that equality of PD0L words (given by their PD0L system) is undecidable. Finally, we show that if erasing morphisms are admitted, then the question of productivity becomes undecidable, that is, the question whether a given PD0L system defines an infinite word.
△ Less
Submitted 10 July, 2012;
originally announced July 2012.
-
On the Complexity of Equivalence of Specifications of Infinite Objects
Authors:
Joerg Endrullis,
Dimitri Hendriks,
Rena Bakhshi
Abstract:
We study the complexity of deciding the equality of infinite objects specified by systems of equations, and of infinite objects specified by lambda-terms. For equational specifications there are several natural notions of equality: equality in all models, equality of the sets of solutions, and equality of normal forms for productive specifications. For lambda-terms we investigate Boehm-tree equali…
▽ More
We study the complexity of deciding the equality of infinite objects specified by systems of equations, and of infinite objects specified by lambda-terms. For equational specifications there are several natural notions of equality: equality in all models, equality of the sets of solutions, and equality of normal forms for productive specifications. For lambda-terms we investigate Boehm-tree equality and various notions of observational equality. We pinpoint the complexity of each of these notions in the arithmetical or analytical hierarchy. We show that the complexity of deciding equality in all models subsumes the entire analytical hierarchy. This holds already for the most simple infinite objects, viz. streams over {0,1}, and stands in sharp contrast to the low arithmetical Pi^0_2-completeness of equality of equationally specified streams derived in [Rosu 2006] employing a different notion of equality.
△ Less
Submitted 30 June, 2012;
originally announced July 2012.
-
Arithmetic Self-Similarity of Infinite Sequences
Authors:
Dimitri Hendriks,
Frits G. W. Dannenberg,
Joerg Endrullis,
Mark Dow,
Jan Willem Klop
Abstract:
We define the arithmetic self-similarity (AS) of a one-sided infinite sequence sigma to be the set of arithmetic progressions through sigma which are a vertical shift of sigma. We study the AS of several famlies of sequences, viz. completely additive sequences, Toeplitz words and Keane's generalized Morse sequences. We give a complete characterization of the AS of completely additive sequences, an…
▽ More
We define the arithmetic self-similarity (AS) of a one-sided infinite sequence sigma to be the set of arithmetic progressions through sigma which are a vertical shift of sigma. We study the AS of several famlies of sequences, viz. completely additive sequences, Toeplitz words and Keane's generalized Morse sequences. We give a complete characterization of the AS of completely additive sequences, and classify the set of single-gap Toeplitz patterns that yield completely additive Toeplitz words. We show that every arithmetic subsequence of a Toeplitz word generated by a one-gap pattern is again a Toeplitz word. Finally, we establish that generalized Morse sequences are specific sum-of-digits sequences, and show that their first difference is a Toeplitz word.
△ Less
Submitted 21 May, 2012; v1 submitted 18 January, 2012;
originally announced January 2012.
-
Automatic Sequences and Zip-Specifications
Authors:
Clemens Grabmayer,
Joerg Endrullis,
Dimitri Hendriks,
Jan Willem Klop,
Lawrence S. Moss
Abstract:
We consider infinite sequences of symbols, also known as streams, and the decidability question for equality of streams defined in a restricted format. This restricted format consists of prefixing a symbol at the head of a stream, of the stream function `zip', and recursion variables. Here `zip' interleaves the elements of two streams in alternating order, starting with the first stream. For examp…
▽ More
We consider infinite sequences of symbols, also known as streams, and the decidability question for equality of streams defined in a restricted format. This restricted format consists of prefixing a symbol at the head of a stream, of the stream function `zip', and recursion variables. Here `zip' interleaves the elements of two streams in alternating order, starting with the first stream. For example, the Thue-Morse sequence is obtained by the `zip-specification' {M = 0 : X, X = 1 : zip(X,Y), Y = 0 : zip(Y,X)}. Our analysis of such systems employs both term rewriting and coalgebraic techniques. We establish decidability for these zip-specifications, employing bisimilarity of observation graphs based on a suitably chosen cobasis. The importance of zip-specifications resides in their intimate connection with automatic sequences. We establish a new and simple characterization of automatic sequences. Thus we obtain for the binary zip that a stream is 2-automatic iff its observation graph using the cobasis (hd,even,odd) is finite. The generalization to zip-k specifications and their relation to k-automaticity is straightforward. In fact, zip-specifications can be perceived as a term rewriting syntax for automatic sequences. Our study of zip-specifications is placed in an even wider perspective by employing the observation graphs in a dynamic logic setting, leading to an alternative characterization of automatic sequences. We further obtain a natural extension of the class of automatic sequences, obtained by `zip-mix' specifications that use zips of different arities in one specification. We also show that equivalence is undecidable for a simple extension of the zip-mix format with projections like even and odd. However, it remains open whether zip-mix specifications have a decidable equivalence problem.
△ Less
Submitted 16 April, 2012; v1 submitted 16 January, 2012;
originally announced January 2012.
-
Transforming Outermost into Context-Sensitive Rewriting
Authors:
Joerg Endrullis,
Dimitri Hendriks
Abstract:
We define two transformations from term rewriting systems (TRSs) to context-sensitive TRSs in such a way that termination of the target system implies outermost termination of the original system. In the transformation based on 'context extension', each outermost rewrite step is modeled by exactly one step in the transformed system. This transformation turns out to be complete for the class of le…
▽ More
We define two transformations from term rewriting systems (TRSs) to context-sensitive TRSs in such a way that termination of the target system implies outermost termination of the original system. In the transformation based on 'context extension', each outermost rewrite step is modeled by exactly one step in the transformed system. This transformation turns out to be complete for the class of left-linear TRSs. The second transformation is called `dynamic labeling' and results in smaller sized context-sensitive TRSs. Here each modeled step is adjoined with a small number of auxiliary steps. As a result state-of-the-art termination methods for context-sensitive rewriting become available for proving termination of outermost rewriting. Both transformations have been implemented in Jambox, making it the most successful tool in the category of outermost rewriting of the last edition of the annual termination competition.
△ Less
Submitted 29 June, 2010; v1 submitted 31 May, 2010;
originally announced May 2010.
-
Modular Construction of Fixed Point Combinators and Clocked Boehm Trees
Authors:
Joerg Endrullis,
Dimitri Hendriks,
Jan Willem Klop
Abstract:
Fixed point combinators (and their generalization: looping combinators) are classic notions belonging to the heart of lambda-calculus and logic. We start with an exploration of the structure of fixed point combinators (fpc's), vastly generalizing the well-known fact that if Y is an fpc, Y(SI) is again an fpc, generating the Boehm sequence of fpc's. Using the infinitary lambda-calculus we devise…
▽ More
Fixed point combinators (and their generalization: looping combinators) are classic notions belonging to the heart of lambda-calculus and logic. We start with an exploration of the structure of fixed point combinators (fpc's), vastly generalizing the well-known fact that if Y is an fpc, Y(SI) is again an fpc, generating the Boehm sequence of fpc's. Using the infinitary lambda-calculus we devise infinitely many other generation schemes for fpc's. In this way we find schemes and building blocks to construct new fpc's in a modular way.
Having created a plethora of new fixed point combinators, the task is to prove that they are indeed new. That is, we have to prove their beta-inconvertibility. Known techniques via Boehm Trees do not apply, because all fpc's have the same Boehm Tree (BT). Therefore, we employ `clocked BT's', with annotations that convey information of the tempo in which the data in the BT are produced. BT's 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 BT-equality, the equality in the classical models of lambda-calculus. An analogous approach pertains to Levy-Longo Berarducci trees. Finally, we increase the discrimination power by a precision of the clock notion that we call `atomic clock'.
△ Less
Submitted 12 February, 2010;
originally announced February 2010.
-
Unique Normal Forms in Infinitary Weakly Orthogonal Term Rewriting
Authors:
Joerg Endrullis,
Clemens Grabmayer,
Dimitri Hendriks,
Jan Willem Klop
Abstract:
The theory of finite and infinitary term rewriting is extensively developed for orthogonal rewrite systems, but to a lesser degree for weakly orthogonal rewrite systems. In this note we present some contributions to the latter case of weak orthogonality, where critial pairs are admitted provided they are trivial.
We start with a refinement of the by now classical Compression Lemma, as a tool f…
▽ More
The theory of finite and infinitary term rewriting is extensively developed for orthogonal rewrite systems, but to a lesser degree for weakly orthogonal rewrite systems. In this note we present some contributions to the latter case of weak orthogonality, where critial pairs are admitted provided they are trivial.
We start with a refinement of the by now classical Compression Lemma, as a tool for establishing infinitary confluence, and hence the property of unique infinitary normal forms, for the case of weakly orthogonal TRSs that do not contain collapsing rewrite rules.
That this restriction of collapse-freeness is crucial, is shown in a elaboration of a simple TRS which is weakly orthogonal, but has two collapsing rules. It turns out that all the usual theory breaks down dramatically.
We conclude with establishing a positive fact: the diamond property for infinitary developments for weakly orthogonal TRSs, by means of a detailed analysis initiated by van Oostrom for the finite case.
△ Less
Submitted 5 November, 2009;
originally announced November 2009.
-
Let's Make a Difference!
Authors:
Joerg Endrullis,
Dimitri Hendriks,
Jan Willem Klop
Abstract:
We study the behaviour of iterations of the difference operator delta on streams over {0,1}. In particular, we show that a stream sigma is eventually periodic if and only if the sequence of differences sigma, delta(sigma), delta(delta(sigma)), ..., the `delta-orbit' of sigma as we call it, is eventually periodic. Moreover, we generalise this result to operations delta_d that sum modulo 2 the ele…
▽ More
We study the behaviour of iterations of the difference operator delta on streams over {0,1}. In particular, we show that a stream sigma is eventually periodic if and only if the sequence of differences sigma, delta(sigma), delta(delta(sigma)), ..., the `delta-orbit' of sigma as we call it, is eventually periodic. Moreover, we generalise this result to operations delta_d that sum modulo 2 the elements of each consecutive block of length d+1 in a given 01-stream. Some experimentation with delta-orbits of well-known streams reveals a surprising connexion between the Sierpinski stream and the Mephisto Waltz.
△ Less
Submitted 5 November, 2009;
originally announced November 2009.
-
Complexity of Fractran and Productivity
Authors:
Joerg Endrullis,
Clemens Grabmayer,
Dimitri Hendriks
Abstract:
In functional programming languages the use of infinite structures is common practice. For total correctness of programs dealing with infinite structures one must guarantee that every finite part of the result can be evaluated in finitely many steps. This is known as productivity. For programming with infinite structures, productivity is what termination in well-defined results is for programmin…
▽ More
In functional programming languages the use of infinite structures is common practice. For total correctness of programs dealing with infinite structures one must guarantee that every finite part of the result can be evaluated in finitely many steps. This is known as productivity. For programming with infinite structures, productivity is what termination in well-defined results is for programming with finite structures.
Fractran is a simple Turing-complete programming language invented by Conway. We prove that the question whether a Fractran program halts on all positive integers is Pi^0_2-complete. In functional programming, productivity typically is a property of individual terms with respect to the inbuilt evaluation strategy. By encoding Fractran programs as specifications of infinite lists, we establish that this notion of productivity is Pi^0_2-complete even for the most simple specifications. Therefore it is harder than termination of individual terms. In addition, we explore possible generalisations of the notion of productivity in the framework of term rewriting, and prove that their computational complexity is Pi^1_1-complete, thus exceeding the expressive power of first-order logic.
△ Less
Submitted 31 July, 2009; v1 submitted 25 March, 2009;
originally announced March 2009.
-
Data-Oblivious Stream Productivity
Authors:
Joerg Endrullis,
Clemens Grabmayer,
Dimitri Hendriks
Abstract:
We are concerned with demonstrating productivity of specifications of infinite streams of data, based on orthogonal rewrite rules. In general, this property is undecidable, but for restricted formats computable sufficient conditions can be obtained. The usual analysis disregards the identity of data, thus leading to approaches that we call data-oblivious. We present a method that is provably opt…
▽ More
We are concerned with demonstrating productivity of specifications of infinite streams of data, based on orthogonal rewrite rules. In general, this property is undecidable, but for restricted formats computable sufficient conditions can be obtained. The usual analysis disregards the identity of data, thus leading to approaches that we call data-oblivious. We present a method that is provably optimal among all such data-oblivious approaches. This means that in order to improve on the algorithm in this paper one has to proceed in a data-aware fashion.
△ Less
Submitted 19 July, 2008; v1 submitted 16 June, 2008;
originally announced June 2008.
