Beta-Reduction As Unification

We define a unification problem ^UP with the property that, given a pure lambda-term M, we can derive an instance Gamma(M) of ^UP from M such that Gamma(M) has a solution if and only if M is beta-strongly normalizable. There is a type discipline for pure lambda-terms that characterizes beta-strong normalization; this is the system of intersection types (without a "top" type that can be assigned to every lambda-term). In this report, we use a lean version LAMBDA of the usual system of intersection types. Hence, ^UP is also an appropriate unification problem to characterize typability of lambda-terms in LAMBDA. It also follows that ^UP is an undecidable problem, which can in turn be related to semi-unification and second-order unification (both known to be undecidable).

Measuring Bottleneck Bandwidth of Targeted Path Segments

Accurate measurement of network bandwidth is crucial for flexible Internet applications and protocols which actively manage and dynamically adapt to changing utilization of network resources. These applications must do so to perform tasks such as distributing and delivering high-bandwidth media, scheduling service requests and performing admission control. Extensive work has focused on two approaches to measuring bandwidth: measuring it hop-by-hop, and measuring it end-to-end along a path. Unfortunately, best-practice techniques for the former are inefficient and techniques for the latter are only able to observe bottlenecks visible at end-to-end scope. In this paper, we develop and simulate end-to-end probing methods which can measure bottleneck bandwidth along arbitrary, targeted subpaths of a path in the network, including subpaths shared by a set of flows. As another important contribution, we describe a number of practical applications which we foresee as standing to benefit from solutions to this problem, especially in emerging, flexible network architectures such as overlay networks, ad-hoc networks, peer-to-peer architectures and massively accessed content servers.