SearcharxivSearch

arXiv subjects

Christophe Raffalli

Publications and source records attributed to Christophe Raffalli.

7 recordsLinked to original sources

Isotopic piecewise affine approximation of algebraic or $C^1$ varieties

We propose a novel sufficient condition establishing that a piecewise affine variety has the same topology as a variety of the sphere $\mathbb{S}^n$ defined by positively homogeneous $C^1$ functions. This covers the case of $C^1$ varieties in the projective space $\mathbb{P}^n$. We prove that this condition is sufficient in the case of codimension one and arbitrary dimension. We describe an implementation working for homogeneous polynomials in arbitrary dimension and codimension and give experimental evidences that our condition might still be sufficient in codimension greater than one.

math.AG

On a question of supports

We give a sufficient condition in order that $n$ closed connected subsets in the $n$-dimensional real projective space admit a common multitangent hyperplane.

math.AG

Abstract Representation of Binders in OCaml using the Bindlib Library

The Bindlib library for OCaml provides a set of tools for the manipulation of data structures with variable binding. It is very well suited for the representation of abstract syntax trees, and has already been used for the implementation of half a dozen languages and proof assistants (including a new version of the logical framework Dedukti). Bindlib is optimised for fast substitution, and it supports variable renaming. Since the representation of binders is based on higher-order abstract syntax, variable capture cannot arise during substitution. As a consequence, variable names are not updated at substitution time. They can however be explicitly recomputed to avoid "visual capture" (i.e., distinct variables with the same apparent name) when a data structure is displayed.

cs.PL

Practical Subtyping for System F with Sized (Co-)Induction

We present a rich type system with subtyping for an extension of System F. Our type constructors include sum and product types, universal and existential quantifiers, inductive and coinductive types. The latter two size annotations allowing the preservation of size invariants. For example it is possible to derive the termination of the quicksort by showing that partitioning a list does not increase its size. The system deals with complex programs involving mixed induction and coinduction, or even mixed (co-)induction and polymorphism (as for Scott-encoded datatypes). One of the key ideas is to completely separate the induction on sizes from the notion of recursive programs. We use the size change principle to check that the proof is well-founded, not that the program terminates. Termination is obtained by a strong normalization proof. Another key idea is the use symbolic witnesses to handle quantifiers of all sorts. To demonstrate the practicality of our system, we provide an implementation that accepts all the examples discussed in the paper and much more.

cs.LO

Distance to the discriminant

We will study algebraic hyper-surfaces on the real unit sphere $\mathcal S^{n-1}$ given by an homogeneous polynomial of degree d in n variables with the view point, rarely exploited, of Euclidian geometry using Bombieri's scalar product and norm. This view point is mostly present in works about the topology of random hyper-surfaces \cite{ShubSmale93, GayetWelschinger14}. Our first result (lemma \ref{distgen} page \pageref{distgen}) is a formula for the distance $\dist(P,Δ)$ of a polynomial to the {\em real discriminant} $Δ$, i.e. the set of polynomials with a real singularity on the sphere. This formula is given for any distance coming from a scalar product on the vector space of polynomials. Then, we concentrate on Bombieri scalar product and its remarkable properties. For instance we establish a combinatoric formula for the scalar product of two products of linear-forms (lemma \ref{scalarlinear} page \pageref{scalarlinear}) which allows to give a (new ?) proof of the invariance of Bombieri's norm by composition with the orthogonal group. These properties yield a simple formula for the distance in theorem \ref{bombineqdist} page \pageref{bombineqdist} from which we deduce the following inequality: $$\dist(P, Δ) \leq \min_{x \hbox{ critical point of } P \hbox{ on } \mathcal S^{n-1}} |P(x)|$$ The definition \ref{maindef} page \pageref{maindef} classifies in two categories the ways to make a polynomial singular to realise the distance to the discriminant. Then, we show, in theorem \ref{extremal} page \pageref{extremal}, that one of the category is forbidden in the case of an {\em extremal} hyper-surfaces (i.e. with maximal Betti numbers). This implies as a corollary \ref{bombeqdistbis} (page \pageref{bombeqdistbis}) that the above inequality becomes an equality is that case. The main result in this paper concerns extremal hyper-surfaces $P=0$ that maximise the distance to the discriminant (with $\|P\| = 1$). They are very remarkable objects which enjoy properties similar to those of quadratic forms: they are linear combination of powers of linear forms $x \mapsto \langle x | u_i \rangle^d$ where the vectors $u_i$ are the critical points of $P$ on $\mathcal S^{n-1}$ corresponding to the least positive critical value of $|P|$. This is corollary \ref{comblinbis} page \pageref{comblinbis} of a similar theorem \ref{comblin} page \pageref{comblin} for all algebraic hyper-surfaces. The next section is devoted to homogeneous polynomials in $2$ variables. We prove that a polynomial of degree $d$ with $2d$ regularly spaced roots on the unit circle is a local maximum of the distance to the discriminant among polynomials with the same norm and number of roots. We conjecture that it is a global maximum and that the polynomial of degree $d$ with $2r$ regularly spaced roots on the unit circle is also a similar global maximum when $d < r \leq 2d$. This claim is supported by the fact that we were able to prove the consequence of this together with corollary \ref{comblinbis} which yields to interesting trigonometric identities that we could not find somewhere else (proposition \ref{trigo} page \pageref{trigo}). We also obtain metric information about algebraic hyper-surfaces. First, in the case of extremal hyper-surface, we give an upper bound (theorem \ref{bandwidth} page \pageref{bandwidth}) on the length of an integral curve of the gradient of $P$ in the band where $|P|$ is less that the least positive critical value of $|P|$. Then, a general lower bound on the size and distance between the connected components of the zero locus of $P$ (corollary \ref{sphereinside} and theorem \ref{distancebetween}). The last section will present experimental results among which are five extremal sextic curves far from the discriminant. These are obtained by very long running numerical optimisation (many months) some of which are not terminated.

math.AG

Asymptotically almost all λ-terms are strongly normalizing

We present quantitative analysis of various (syntactic and behavioral) properties of random λ-terms. Our main results are that asymptotically all the terms are strongly normalizing and that any fixed closed term almost never appears in a random term. Surprisingly, in combinatory logic (the translation of the λ-calculus into combinators), the result is exactly opposite. We show that almost all terms are not strongly normalizing. This is due to the fact that any fixed combinator almost always appears in a random combinator.

math.LO