Set Comprehension in Church's Type Theory

Chad E. Brown
 

In order to prove theorems involving sets and functions, one often uses comprehension principles asserting the existence of certain sets. We explore the consequences of restricting which logical constants are allowed in these comprehension principles in the context of Church's type theory. Church's type theory is a formulation of higher-order logic that allows quantification over sets and functions. In this logic, any set definable by an expression of the language can be proved to exist. This expressive power allows a natural formalization of much of mathematics. The logical constants we consider are propositional connectives, equality and quantifiers over various types. For example, we consider fragments of Church's type theory which satisfy comprehension with respect to quantifiers over individuals, but not over sets of individuals. There are natural sequent calculi and corresponding semantics for any given signature. In some cases, adding logical constants to a signature does not increase the set of theorems (giving conservation results). In other cases, adding logical constants does increase the set of theorems (giving independence results). We establish these results using models of fragments of type theory. For example, the usual proof of Cantor's theorem that there is no surjection from a set S onto its power set P(S) uses a diagonal set whose definition involves a negation. We construct a model showing that this theorem cannot be proven in a fragment of Church's type theory which lacks comprehension principles involving negation. To prove the version of Cantor's theorem that there is no injection from P(S) into S requires comprehension principles involving quantifiers over sets in P(S) and equality of objects in S as well as negation.

***********************************************************************

Autonomous Fast Classifiers For Pharmaceutical Data Sets.

Paul Komarek

Deciding which classification tool is best suited to a data set can be time consuming, and distracts researchers from larger scientific and business objectives. Running multiple cross-validations to compare well-understood, traditional statistical methods has become increasingly difficult as data sets grow larger. Logistic regression and k-nearest neighbor are two examples of familiar techniques that have been described as too slow for modern data mining and classification problems. We will explain how we accelerated these methods, making them suitable for large biopharmaceutical datasets. Our logistic regression implementation requires little or no tuning, scores on par with or better than RBF SVMs, and often runs at least twice as fast as linear SVMs. This level of performance makes it realistic to experiment with large data sets until satisfactory results are obtained. Our software is available from http://www.autonlab.org.

***********************************************************************
 

Hamilton cycles in random graphs

Kelley Burgin

***********************************************************************
 

Creating a Giant Component

David Kravitz

The problem of taking cn random edges on n vertices is well-studied. Instead of this, we will look at cn pairs of random edges, and using several different algorithms we will choose one edge from each pair, trying to create a giant component with high probability as fast as possible. We show an on-line algorithm that creates a giant by c=0.38, existence of an off-line algorithm which achieves the best possible c=0.25, and a lower bound greater than 0.25 for all on-line algorithms. In addition, we have a sharp threshold for a large class of on-line algorithms. Joint work with Tom Bohman.

***********************************************************************

Update your Portfolio: new elements on the work of Harry Markowitz

Juan Carlos Rivera

The classical problem of portfolio choice proposed by Markowitz is revisited with some changes involving current mathematical finance tools; continuous-time markets and coherent risk measures. Also, a risk manager's perspective is added to the model of the investment. Under the current methodology, the problem is equivalent to an stochastic control problem with constraints in proportions of capital invested.

***********************************************************************

Juan Vera

Recently there has been much interest in understanding the properties of real-world large-scale networks such as the Internet graphs, social networks and biological networks. Experimental studies have demonstrated that a large variety of these networks present a power law degree distribution. The classical models of random graphs do not exhibit this distribution, so they are not suitable for modeling these networks. One approach that have had much success in reproducing power laws is the use of preferential attachment to generate the random graph. The vertices appear one at a time and choose its neighbors among the existing vertices with probability proportional to their degree. We consider the robustness of this model. First, we analyze an evolving network that sometimes loses vertices at random. Secondly we study the case when the network is "attacked" by a player who decides which vertices to delete. Joint work with Alan Frieze and Abie Flaxman

***********************************************************************

Cristina Popovici

A Gamma-convergence result for non-convex functionals of vector-valued functions arising in the study of coupled singular perturbations for phase transitions is obtained in the case where the energy density has two potential wells. Joint work with Irene Fonseca.

***********************************************************************

Margarida Baia

We seek to characterize the asymptotic behavior of a family of functionals with periodic integrands.
Using techniques of 2-scale convergence, and under standard coercivity and growth conditions, we are able to treat the nonconvex case through Gamma-convergence arguments assuming that the integrand f=f(x,y,z) is measurable in x, continuous with respect to the pair (y,z), and (0,1)^N-periodic as a function of the variable y.
Joint work with Irene Fonseca.

***********************************************************************

Luca Petrelli

The original Monge's problem consisted in transporting a pile of soil to an excavation fill. He formulated the related mathematical problem in 1781. This is still an open problem in its full generality. In the 1940's Kantorovich proposed and solved a relaxation of Monge's problem, for which he was awarded a Nobel prize in Economy for his work in "optimal allocation of resources". Key to his result was the corresponding dual problem. In this talk I will give an overview of the history and main characteristics of the Monge-Kantorovich problem and of its dual. I will then show how Partial Differential Equations can be related to mass transportation theory through the gradient flow formalism. I will also discuss recent advances in the field including an application to nonlinear diffusion problems.