arXiv subjects

Trifon Trifonov

Publications and source records attributed to Trifon Trifonov.

72 records · Page 4Linked to original sources

arXiv2019

TOI-677 b: A Warm Jupiter (P=11.2d) on an eccentric orbit transiting a late F-type star

We report the discovery of TOI-677 b, first identified as a candidate in light curves obtained within Sectors 9 and 10 of the Transiting Exoplanet Survey Satellite (TESS) mission and confirmed with radial velocities. TOI-677 b has a mass of M_p = 1.236$^{+0.069}_{-0.067}$ M_J, a radius of R_p = 1.170 +- 0.03 R_J,and orbits its bright host star (V=9.8 mag) with an orbital period of 11.23660 +- 0.00011 d, on an eccentric orbit with e = 0.435 +- 0.024. The host star has a mass of M_* = 1.181 +- 0.058 M_sun, a radius of R_* = 1.28 +- 0.03 R_sun, an age of 2.92$^{+0.80}_{-0.73}$ Gyr and solar metallicity, properties consistent with a main sequence late F star with T_eff = 6295 +- 77 K. We find evidence in the radial velocity measurements of a secondary long term signal which could be due to an outer companion. The TOI-677 b system is a well suited target for Rossiter-Mclaughlin observations that can constrain migration mechanisms of close-in giant planets.

astro-ph.EP↗

arXiv2019

Variables in the Southern Polar Region Evryscope 2016 Dataset

The regions around the celestial poles offer the ability to find and characterize long-term variables from ground-based observatories. We used multi-year Evryscope data to search for high-amplitude (~5% or greater) variable objects among 160,000 bright stars (Mv < 14.5) near the South Celestial Pole. We developed a machine learning based spectral classifier to identify eclipse and transit candidates with M-dwarf or K-dwarf host stars - and potential low-mass secondary stars or gas giant planets. The large amplitude transit signals from low-mass companions of smaller dwarf host stars lessens the photometric precision and systematics removal requirements necessary for detection, and increases the discoveries from long-term observations with modest light curve precision. The Evryscope is a robotic telescope array that observes the Southern sky continuously at 2-minute cadence, searching for stellar variability, transients, transits around exotic stars and other observationally challenging astrophysical variables. In this study, covering all stars 9 < Mv < 14.5, in declinations -75 to -90 deg, we recover 346 known variables and discover 303 new variables, including 168 eclipsing binaries. We characterize the discoveries and provide the amplitudes, periods, and variability type. A 1.7 Jupiter radius planet candidate with a late K-dwarf primary was found and the transit signal was verified with the PROMPT telescope network. Further followup revealed this object to be a likely grazing eclipsing binary system with nearly identical primary and secondary K5 stars. Radial velocity measurements from the Goodman Spectrograph on the 4.1 meter SOAR telescope of the likely-lowest-mass targets reveal that six of the eclipsing binary discoveries are low-mass (.06 - .37 solar mass) secondaries with K-dwarf primaries, strong candidates for precision mass-radius measurements.

astro-ph.SR↗

arXiv2019

Precise radial velocities of giant stars. XI. Two brown dwarfs in 6:1 mean motion resonance around the K giant star $ν$ Ophiuchi

We present radial-velocity (RV) measurements for the K giant $ν$ Oph (= HIP88048, HD163917, HR6698), which reveal two brown dwarf companions with a period ratio close to 6:1. For our orbital analysis we use 150 precise RV measurements taken at Lick Observatory between 2000 and 2011, and we combine them with RV data for this star available in the literature. Using a stellar mass of $M = 2.7\,M_\odot$ for $ν$ Oph and applying a self-consistent N-body model we estimate the minimum dynamical companion masses to be $m_1\sin i \approx 22.2\,M_{\mathrm{Jup}}$ and $m_2\sin i \approx 24.7\,M_{\mathrm{Jup}}$, with orbital periods $P_1 \approx 530$ d and $P_2 \approx 3185$ d. We study a large set of potential orbital configurations for this system, employing a bootstrap analysis and a systematic $χ_ν^2$ grid-search coupled with our dynamical fitting model, and we examine their long-term stability. We find that the system is indeed locked in a 6:1 mean motion resonance (MMR), with $Δω$ and all six resonance angles $θ_{1}, \ldots, θ_{6}$ librating around 0$^\circ$. We also test a large set of coplanar inclined configurations, and we find that the system will remain in a stable resonance for most of these configurations. The $ν$ Oph system is important for probing planetary formation and evolution scenarios. It seems very likely that the two brown dwarf companions of $ν$ Oph formed like planets in a circumstellar disk around the star and have been trapped in a MMR by smooth migration capture.

astro-ph.SR↗

arXiv2019

Precise radial velocities of giant stars. XII. Evidence against the proposed planet Aldebaran b

Radial-velocity variations of the K giant star Aldebaran ($α$ Tau) were first reported in the early 1990s. After subsequent analyses, the radial-velocity variability with a period of $\sim 629\,\mathrm{d}$ has recently been interpreted as caused by a planet of several Jovian masses. We want to further investigate the hypothesis of an extrasolar planet around Aldebaran. We combine 165 new radial-velocity measurements from Lick Observatory with seven already published data sets comprising 373 radial-velocity measurements. We perform statistical analyses and investigate whether a Keplerian model properly fits the radial velocities. We also perform a dynamical stability analysis for a possible two-planet solution. As best Keplerian fit to the combined radial-velocity data we obtain an orbit for the hypothetical planet with a smaller period ($P=607\,\mathrm{d}$) and a larger eccentricity ($e=0.33 \pm 0.04$) than the previously proposed one. However, the residual scatter around that fit is still large, with a standard deviation of $117\,\mathrm{ms}^{-1}$. In 2006/2007, the statistical power of the $\sim 620\,\mathrm{d}$ period showed a temporary but significant decrease. Plotting the growth of power in reverse chronological order reveals that a period around $620\,\mathrm{d}$ is clearly present in the newest data but not in the data taken before $\sim$ 2006. Furthermore, an apparent phase shift between radial-velocity data and orbital solution is observable at certain times. A two-planet Keplerian fit matches the data considerably better than a single-planet solution, but poses severe dynamical stability issues. The radial-velocity data from Lick Observatory do not further support but in fact weaken the hypothesis of a substellar companion around Aldebaran. Oscillatory convective modes might be a plausible alternative explanation of the observed radial-velocity variations.

astro-ph.SR↗

arXiv2019

TESS exoplanet candidates validated with HARPS archival data. A massive Neptune around GJ143 and two Neptunes around HD23472

We aim at the discovery of new planetary systems by exploiting the transit light curve results from TESS orbital observatory's Sector 1 and 2 observations and validating them with precise Doppler measurements obtained from archival HARPS data. Taking advantage of the reported TESS transit events around GJ143 (TOI 186) and HD23472 (TOI 174) we model their HARPS precise Doppler measurements and derive orbital parameters for these two systems. For the GJ143 system TESS has reported only a single transit, and thus its period is unconstrained from photometry. Our RV analysis of GJ143 reveal the full Keplerian solution of the system, which is consistent with an eccentric planet with a mass almost twice that of Neptune and a period of $P_{\rm b}$ = $35.59_{-0.01}^{+0.01}$ days. Our estimates of the GJ143 b planet are fully consistent with the transit timing from TESS. We confirm the two-planet system around HD23472, which according to our analysis is composed of two Neptune mass planets in a possible 5:3 MMR.

astro-ph.EP↗

arXiv2019

Correcting HIRES radial velocities for small systematic errors

The HIRES spectrograph, mounted on the $10$-m Keck-I telescope, belongs to a small group of radial-velocity (RV) instruments that produce stellar RVs with long-term precision down to $\sim1$ ms$^{-1}$. In $2017$, the HIRES team published $64,480$ RVs of $1,699$ stars, collected between $1996$ and $2014$. In this bank of RVs, we identify a sample of RV-quiet stars, whose RV scatter is $<10$ ms$^{-1}$, and use them to reveal two small but significant nightly zero-point effects: a discontinuous jump, caused by major modifications of the instrument in August $2004$, and a long-term drift. The size of the $2004$ jump is $1.5\pm0.1$ ms$^{-1}$, and the slow zero-point variations have a typical magnitude of $\lesssim1$ ms$^{-1}$. In addition, we find a small but significant correlation between stellar RVs and the time relative to local midnight, indicative of an average intra-night drift of $0.051\pm0.004$ ms$^{-1}$hr$^{-1}$. We correct the $64,480$ HIRES RVs for the systematic effects we find, and make the corrected RVs publicly available. Our findings demonstrate the importance of observing RV-quiet stars, even in the era of simultaneously-calibrated RV spectrographs. We hope that the corrected HIRES RVs will facilitate the search for new planet candidates around the observed stars.

astro-ph.EP↗

arXiv2019

Two Jovian planets around the giant star HD202696. A growing population of packed massive planetary pairs around massive stars?

We present evidence for a new two-planet system around the giant star HD202696 (= HIP105056, BD+26 4118). The discovery is based on public HIRES radial velocity measurements taken at Keck Observatory between July 2007 and September 2014. We estimate a stellar mass of 1.91$^{+0.09}_{-0.14}M_\odot$ for HD202696, which is located close to the base of the red giant branch. A two-planet self-consistent dynamical modeling MCMC scheme of the radial velocity data followed by a long-term stability test suggests planetary orbital periods of $P_{\rm b}$ = 517.8$_{-3.9}^{+8.9}$ days and $P_{\rm c}$ = 946.6$_{-20.9}^{+20.7}$ days, eccentricities of $e_{\rm b}$ = 0.011$_{-0.011}^{+0.078}$ and $e_{\rm c}$ = 0.028$_{-0.012}^{+0.065}$ , and minimum dynamical masses of $m_{\rm b}$ = 2.00$_{-0.10}^{+0.22}$\,$M_{\mathrm{Jup}}$ and $m_{\rm c}$ = 1.86$_{-0.23}^{+0.18}$,$M_{\mathrm{Jup}}$, respectively. Our stable MCMC samples are consistent with orbital configurations predominantly in a mean period ratio of 11:6 and its close-by high order mean-motion commensurabilities with low eccentricities. For the majority of the stable configurations we find an aligned or anti-aligned apsidal libration (i.e.\ $Δω$ librating around 0$^\circ$ or 180$^\circ$), suggesting that the HD202696 system is likely dominated by secular perturbations near the high-order 11:6 mean-motion resonance. The HD202696 system is yet another Jovian mass pair around an intermediate mass star with a period ratio below the 2:1 mean motion resonance. Therefore, the HD202696 system is an important discovery, which may shed light on the primordial disk-planet properties needed for giant planets to break the strong 2:1 mean motion resonance and settle in more compact orbits.

astro-ph.EP↗

arXiv2018

New HARPS and FEROS observations of GJ1046

In this paper we present new precise Doppler data of GJ1046 taken between November 2005 and July 2018 with the HARPS and the FEROS high-resolution spectographs. In addition, we provide a new stellar mass estimate of GJ1046 and we update the orbital parameters of the GJ1046 system. These new data and analysis could be used together with the GAIA epoch astrometry, when available, for braking the $\sin i$ degeneracy and revealing the true mass of the GJ1046 system.

astro-ph.EP↗

arXiv2018

HD 202772A B: A Transiting Hot Jupiter Around A Bright, Mildly Evolved Star In A Visual Binary Discovered By Tess

We report the first confirmation of a hot Jupiter discovered by the Transiting Exoplanet Survey Satellite (TESS) mission: HD 202772A b. The transit signal was detected in the data from TESS Sector 1, and was confirmed to be of planetary origin through radial-velocity measurements. HD 202772A b is orbiting a mildly evolved star with a period of 3.3 days. With an apparent magnitude of V = 8.3, the star is among the brightest known to host a hot Jupiter. Based on the 27days of TESS photometry, and radial velocity data from the CHIRON and HARPS spectrographs, the planet has a mass of 1.008+/-0.074 M_J and radius of 1.562+/-0.053 R_J , making it an inflated gas giant. HD 202772A b is a rare example of a transiting hot Jupiter around a quickly evolving star. It is also one of the most strongly irradiated hot Jupiters currently known.

astro-ph.EP↗

arXiv2018

The CARMENES search for exoplanets around M dwarfs: A low-mass planet in the temperate zone of the nearby K2-18

K2-18 is a nearby M2.5 dwarf, located at 34 pc and hosting a transiting planet which was first discovered by the {\it K2} mission and later confirmed with {\it Spitzer Space Telescope} observations. With a radius of $\sim 2 \, R_{\oplus}$ and an orbital period of $\sim 33$ days, the planet lies in the temperate zone of its host star and receives stellar irradiation similar to Earth. Here we perform radial velocity follow-up observations with the visual channel of CARMENES with the goal of determining the mass and density of the planet. We measure a planetary semi-amplitude of $K_b \sim 3.5$ \mpersec\ and a mass of $M_b \sim 9 \, M_{\oplus}$, yielding a bulk density around $ρ_b \sim 4 \, \mathrm{g \,cm^{-3}}$. This indicates a low-mass planet with a composition consistent with a solid core and a volatile-rich envelope. A signal at 9 days was recently reported using radial velocity measurements taken with the HARPS spectrograph. This was interpreted as being due to a second planet. We see a weaker, time and wavelength dependent signal in the CARMENES data set and thus favor stellar activity for its origin. \ktwo\ joins the growing group of low-mass planets detected in the temperate zone of M dwarfs. The brightness of the host star in the near-infrared makes the system a good target for detailed atmospheric studies with the {\it James Webb Space Telescope}.

astro-ph.EP↗

arXiv2018

Dynamical analysis of the circumprimary planet in the eccentric binary system HD59686

We present a detailed orbital and stability analysis of the HD~59686 binary-star planet system. HD~59686 is a single-lined moderately close ($a_{B} = 13.6\,$AU) eccentric ($e_{B} = 0.73$) binary, where the primary is an evolved K giant with mass $M = 1.9 M_{\odot}$ and the secondary is a star with a minimum mass of $m_{B} = 0.53 M_{\odot}$. Additionally, on the basis of precise radial velocity (RV) data a Jovian planet with a minimum mass of $m_p = 7 M_{\mathrm{Jup}}$, orbiting the primary on a nearly circular S-type orbit with $e_p = 0.05$ and $a_p = 1.09\,$AU, has recently been announced. We investigate large sets of orbital fits consistent with HD 59686's radial velocity data by applying bootstrap and systematic grid-search techniques coupled with self-consistent dynamical fitting. We perform long-term dynamical integrations of these fits to constrain the permitted orbital configurations. We find that if the binary and the planet in this system have prograde and aligned coplanar orbits, there are narrow regions of stable orbital solutions locked in a secular apsidal alignment with the angle between the periapses, $Δω$, librating about $0^\circ$. We also test a large number of mutually inclined dynamical models in an attempt to constrain the three-dimensional orbital architecture. We find that for nearly coplanar and retrograde orbits with mutual inclination $145^\circ \lesssim Δi \leq 180^\circ$, the system is fully stable for a large range of orbital solutions.

astro-ph.EP↗

arXiv2016

Precise radial velocities of giant stars IX. HD 59686 Ab: a massive circumstellar planet orbiting a giant star in a ~13.6 au eccentric binary system

Context: For over 12 yr, we have carried out a precise radial velocity survey of a sample of 373 G and K giant stars using the Hamilton Échelle Spectrograph at Lick Observatory. There are, among others, a number of multiple planetary systems in our sample as well as several planetary candidates in stellar binaries. Aims: We aim at detecting and characterizing substellar+stellar companions to the giant star HD 59686 A (HR 2877, HIP 36616). Methods: We obtained high precision radial velocity (RV) measurements of the star HD 59686 A. By fitting a Keplerian model to the periodic changes in the RVs, we can assess the nature of companions in the system. In order to discriminate between RV variations due to non-radial pulsation or stellar spots we used infrared RVs taken with the CRIRES spectrograph at the Very Large Telescope. Additionally, to further characterize the system, we obtain high-resolution images with LMIRCam at the Large Binocular Telescope. Results: We report the likely discovery of a giant planet with a mass of $m_{p}~\sin i=6.92_{-0.24}^{+0.18}~M_{Jup}$ orbiting at $a_{p}=1.0860_{-0.0007}^{+0.0006}$ au from the giant star HD 59686 A. Besides the planetary signal, we discover an eccentric ($e_{B}=0.729_{-0.003}^{+0.004}$) binary companion with a mass of $m_{B}~\sin i=0.5296_{-0.0008}^{+0.0011}~M_{Sun}$ orbiting at a semi-major axis of just $a_{B}=13.56_{-0.14}^{+0.18}$ au. Conclusions: The existence of the planet HD 59686 Ab in a tight eccentric binary system severely challenges standard giant planet formation theories and requires substantial improvements to such theories in tight binaries. Otherwise, alternative planet formation scenarios such as second generation planets or dynamical interactions in an early phase of the system's lifetime should be seriously considered in order to better understand the origin of this enigmatic planet.

astro-ph.EP↗

arXiv2015

Precise radial velocities of giant stars VIII. Testing for the presence of planets with CRIRES Infrared Radial Velocities

We have been monitoring 373 very bright (V < 6 mag) G and K giants with high precision optical Doppler spectroscopy for more than a decade at Lick Observatory. Our goal was to discover planetary companions around those stars and to better understand planet formation and evolution around intermediate-mass stars. However, in principle, long-term, g-mode nonradial stellar pulsations or rotating stellar features, such as spots, could effectively mimic a planetary signal in the radial velocity data. Our goal is to compare optical and infrared radial velocities for those stars with periodic radial velocity patterns and to test for consistency of their fitted radial velocity semiamplitudes. Thereby, we distinguish processes intrinsic to the star from orbiting companions as reason for the radial velocity periodicity observed in the optical. Stellar spectra with high spectral resolution have been taken in the H-band with the CRIRES near-infrared spectrograph at ESO's VLT for 20 stars of our Lick survey. Radial velocities are derived using many deep and stable telluric CO2 lines for precise wavelength calibration. We find that the optical and near-infrared radial velocities of the giant stars in our sample are consistent. We present detailed results for eight stars in our sample previously reported to have planets or brown dwarf companions. All eight stars passed the infrared test. We conclude that the planet hypothesis provides the best explanation for the periodic radial velocity patterns observed for these giant stars.

astro-ph.EP↗

arXiv2015

Disentangling 2:1 resonant radial velocity orbits from eccentric ones and a case study for HD 27894

In radial velocity observations, a pair of extrasolar planets near a 2:1 orbital resonance can be misinterpreted as a single eccentric planet, if data are sparse and measurement precision insufficient to distinguish between these models. We determine the fraction of alleged single-planet RV detected systems for which a 2:1 resonant pair of planets is also a viable model and address the question of how the models can be disentangled. By simulation we quantified the mismatch arising from applying the wrong model. Model alternatives are illustrated using the supposed single-planet system HD 27894 for which we also study the dynamical stability of near-2:1 resonant solutions. From the data scatter around the fitted single-planet Keplerians, we find that for $74\% $ of the $254$ putative single-planet systems, a 2:1 resonant pair cannot be excluded as a viable model, since the error due to the wrong model is smaller than the scatter. For $187$ stars $χ^2$-probabilities can be used to reject the Keplerian models with a confidence of $95\% $ for $54\% $ of the stars and with $99.9\% $ for $39\% $ of the stars. For HD 27894 a considerable fit improvement is obtained when adding a low-mass planet near half the orbital period of the known Jovian planet. Dynamical analysis demonstrates that this system is stable when both planets are initially placed on circular orbits. For fully Keplerian orbits a stable system is only obtained if the eccentricity of the inner planet is constrained to $<0.3$. A large part of the allegedly RV detected single-planet systems should be scrutinized in order to determine the fraction of systems containing near-2:1 resonant pairs of planets. Knowing the abundance of such systems will allow us to revise the eccentricity distribution for extrasolar planets and provide direct constraints for planetary system formation.

astro-ph.SR↗

arXiv2014

Precise Radial Velocities of Giant Stars VII. Occurrence Rate of Giant Extrasolar Planets as a Function of Mass and Metallicity

(abridged) We have obtained precise radial velocities for a sample of 373 G and K type giants at Lick Observatory regularly over more than 12 years. Planets have been identified around 15 giant stars; an additional 20 giant stars host planet candidates. We investigate the occurrence rate of substellar companions around giant stars as a function of stellar mass and metallicity. We probe the stellar mass range from about 1 to beyond 3 M_Sun, which is not being explored by main-sequence samples. We fit the giant planet occurrence rate as a function of stellar mass and metallicity with a Gaussian and an exponential distribution, respectively. We find strong evidence for a planet-metallicity correlation among the secure planet hosts of our giant star sample, in agreement with the one for main-sequence stars. However, the planet-metallicity correlation is absent for our sample of planet candidates, raising the suspicion that a good fraction of them might indeed not be planets. Consistent with the results obtained by Johnson for subgiants, the giant planet occurrence rate increases in the stellar mass interval from 1 to 1.9 M_Sun. However, there is a maximum at a stellar mass of 1.9 +0.1/-0.5 M_Sun, and the occurrence rate drops rapidly for masses larger than 2.5-3.0 M_Sun. We do not find any planets around stars more massive than 2.7 M_Sun, although there are 113 stars with masses between 2.7 and 5 M_Sun in our sample (corresponding to a giant planet occurrence rate < 1.6% at 68.3% confidence in that stellar mass bin). We also show that this result is not a selection effect related to the planet detectability being a function of the stellar mass. We conclude that giant planet formation or inward migration is suppressed around higher mass stars, possibly because of faster disk depletion coupled with a longer migration timescale.

astro-ph.EP↗

arXiv2014

Precise radial velocities of giant stars VI. A possible 2:1 resonant planet pair around the K giant star $η$ Cet

We report the discovery of a new planetary system around the K giant $η$ Cet (HIP 5364, HD 6805) based on 118 high-precision optical radial velocities taken at Lick Observatory since July 2000. Since October 2011 an additional nine near-infrared Doppler measurements have been taken using the ESO CRIRES spectrograph (VLT, UT1). The visible data set shows two clear periodicities. Although we cannot completely rule out that the shorter period is due to rotational modulation of stellar features, the infrared data show the same variations as in the optical, which strongly supports that the variations are caused by two planets. Assuming the mass of $η$ Cet to be 1.7 $M_\odot$, the best edge-on coplanar dynamical fit to the data is consistent with two massive planets ($m_b\sin i$ = 2.6 $\pm$ 0.2 $M_{\mathrm{Jup}}$, $m_c\sin i$ = 3.3 $\pm$ 0.2 $M_{\mathrm{Jup}}$), with periods of $P_b$ = 407 $\pm$ 3 days and $P_c$ = 740 $\pm$ 5 days and eccentricities of $e_b$ = 0.12 $\pm$ 0.05 and $e_c$ = 0.08 $\pm$ 0.03. We tested a wide variety of edge-on coplanar and inclined planetary configurations for stability, which agree with the derived radial velocities. We find that in certain coplanar orbital configurations with moderate $e_b$ eccentricity, the planets can be effectively trapped in an anti-aligned 2:1 mean motion resonance. A much larger non-resonant stable region exists in low-eccentricity parameter space, although it appears to be much farther from the best fit than the 2:1 resonant region. In all other cases, the system is categorized as unstable or chaotic. Another conclusion from the coplanar inclined dynamical test is that the planets can be at most a factor of $\sim$ 1.4 more massive than their suggested minimum masses. This stability constraint on the inclination excludes the possibility of two brown dwarfs, and strongly favors a planetary system.

astro-ph.EP↗

arXiv2012

4MOST - 4-metre Multi-Object Spectroscopic Telescope

The 4MOST consortium is currently halfway through a Conceptual Design study for ESO with the aim to develop a wide-field (>3 square degree, goal >5 square degree), high-multiplex (>1500 fibres, goal 3000 fibres) spectroscopic survey facility for an ESO 4m-class telescope (VISTA). 4MOST will run permanently on the telescope to perform a 5 year public survey yielding more than 20 million spectra at resolution R~5000 (λ=390-1000 nm) and more than 2 million spectra at R~20,000 (395-456.5 nm & 587-673 nm). The 4MOST design is especially intended to complement three key all-sky, space-based observatories of prime European interest: Gaia, eROSITA and Euclid. Initial design and performance estimates for the wide-field corrector concepts are presented. We consider two fibre positioner concepts, a well-known Phi-Theta system and a new R-Theta concept with a large patrol area. The spectrographs are fixed configuration two-arm spectrographs, with dedicated spectrographs for the high- and low-resolution. A full facility simulator is being developed to guide trade-off decisions regarding the optimal field-of-view, number of fibres needed, and the relative fraction of high-to-low resolution fibres. Mock catalogues with template spectra from seven Design Reference Surveys are simulated to verify the science requirements of 4MOST. The 4MOST consortium aims to deliver the full 4MOST facility by the end of 2018 and start delivering high-level data products for both consortium and ESO community targets a year later with yearly increments.

astro-ph.IM↗

arXiv2011

Dialectica Interpretation with Marked Counterexamples

Goedel's functional "Dialectica" interpretation can be used to extract functional programs from non-constructive proofs in arithmetic by employing two sorts of higher-order witnessing terms: positive realisers and negative counterexamples. In the original interpretation decidability of atoms is required to compute the correct counterexample from a set of candidates. When combined with recursion, this choice needs to be made for every step in the extracted program, however, in some special cases the decision on negative witnesses can be calculated only once. We present a variant of the interpretation in which the time complexity of extracted programs can be improved by marking the chosen witness and thus avoiding recomputation. The achieved effect is similar to using an abortive control operator to interpret computational content of non-constructive principles.

cs.LO↗