This paper introduces Brouwerian Type Theory ( \(( {BTT}) \) ), an extension of Constructive Type Theory incorporating Brouwer’s notion of computability to move beyond the Church-Turing paradigm. \( {BTT} \) achieves this by internalizing the notion of choice sequences—dynamic constructs with an evolving temporal nature central to intuitionistic mathematics. To support these constructs, which evolve over time through non-lawlike decisions, in a type system, \( {BTT} \) leverages the concept of bars, inspired by Kripke-style and Beth-style possible-world semantics, which enable structured handling of the temporal progression inherent in choice sequences. This ensures structured handling of evolving states while maintaining type-theoretic properties like transitivity and symmetry, alongside possible-world properties such as monotonicity and locality. The paper examines two concrete types of bars: Beth bars, which require constructing a complete bar to validate types, and open bars, which simplify validity by requiring only local extensions. While the former captures a purely constructive interpretation, the latter is shown to be compatible with classical reasoning, highlighting how varying bar interpretations in \( {BTT} \) affect compatibility with classical reasoning. Finally, the paper demonstrates the robustness of \( {BTT} \) for internalizing choice sequences by validating their core theory.
The logics \(\mathsf {CS4} \) and \(\mathsf {IS4} \) are the two leading intuitionistic variants of the modal logic \(\mathsf {S4} \) . Whether the finite model property holds for each of these logics have been long-standing open problems. In this paper, we resolve the first of these problems, proving that \(\mathsf {CS4} \) has the finite frame property. Additionally, we investigate the following three logics closely related to \(\mathsf {IS4} \) . The logic \(\mathsf {GS4} \) is obtained by adding the Gödel–Dummett axiom to \(\mathsf {IS4} \) ; it is both a superintuitionistic and a fuzzy logic and has previously been given a real-valued semantics. We provide an alternative birelational semantics and prove strong completeness with respect to this semantics. The extension \(\mathsf {GS4}^c \) of \(\mathsf {GS4} \) corresponds to requiring a crisp accessibility relation on the real-valued semantics. We give \(\mathsf {GS4}^c \) a birelational semantics corresponding to an extra confluence condition on the \(\mathsf {GS4} \) birelational semantics and prove strong completeness. Neither of these two logics have the finite model property with respect to their real-valued semantics, but we prove that they have the finite frame property with respect to their birelational semantics. Establishing the finite birelational frame property immediately establishes decidability, which was previously open for these two logics. Our proofs yield coNEXPTIME upper bounds for \(\mathsf {CS4} \) , \(\mathsf {GS4} \) , and \(\mathsf {GS4}^c \) . The logic \(\mathsf {S4I} \) is obtained from \(\mathsf {IS4} \) by reversing the roles of the modal and intuitionistic relations in the birelational semantics. We also prove the finite frame property, and thereby decidability, for \(\mathsf {S4I} \) , although our proof does not yield an elementary complexity bound. In summary, we prove that \(\mathsf {CS4} \) , \(\mathsf {GS4} \) , \(\mathsf {GS4}^c \) , and \(\mathsf {S4I} \) all have the finite birelational frame property, with the first three having a coNEXPTIME validity problem.
We give a simple characterization of the functions that can be computed deterministically by anonymous processes in dynamic networks, depending on the number of leaders in the network. In addition, we provide efficient distributed algorithms for computing all such functions assuming minimal or no knowledge about the network. Each of our algorithms comes in two versions: one that terminates with the correct output and a faster one that stabilizes on the correct output without explicit termination. Notably, these are the first deterministic algorithms whose running times scale linearly with both the number of processes and a parameter of the network which we call"dynamic disconnectivity"(meaning that our dynamic networks do not necessarily have to be connected at all times). We also provide matching lower bounds, showing that all our algorithms are asymptotically optimal for any fixed number of leaders. While most of the existing literature on anonymous dynamic networks relies on classic mass-distribution techniques, our work makes use of a novel combinatorial structure called"history tree", which is of independent interest. Among other contributions, our results make conclusive progress on two popular fundamental problems for anonymous dynamic networks: leaderless Average Consensus (i.e., computing the mean value of input numbers distributed among the processes) and multi-leader Counting (i.e., determining the exact number of processes in the network). Our contribution not only opens a promising line of research on applications of history trees, but also demonstrates that computation in anonymous dynamic networks is practically feasible and far less demanding than previously conjectured.
In traditional algorithm design, no incentives come into play: the input is given, and your algorithm must produce a correct output. How much harder is it to solve the same problem when the input is not given directly, but instead reported by strategic agents with interests of their own? The unique challenge stems from the fact that the agents may choose to lie about the input in order to manipulate the behavior of the algorithm for their own interests, and tools from Game Theory are, therefore, required in order to predict how these agents will behave. We develop a new algorithmic framework with which to study such problems. Specifically, we provide a computationally efficient black-box reduction from solving any Bayesian optimization problem on “strategic input,” often called algorithmic mechanism design , to solving a perturbed version of that same optimization problem when the input is directly given, traditionally called algorithm design . We further demonstrate the power of our framework by making significant progress on several long-standing open problems. First, we provide an algorithmic extension of Myerson’s celebrated characterization of single item auctions [ 105 ] to multiple items, providing also a computationally efficient implementation of optimal auctions. Next, we design a computationally efficient 2-approximate mechanism for Bayesian job scheduling on unrelated machines, the original problem studied in Nisan and Ronen’s seminal article introducing the field of Algorithmic Mechanism Design [ 106 ]. This matches the guarantee of the best known computationally efficient algorithm when the input is directly given. Finally, leveraging a connection to our framework, we additionally prove hardness of approximation for Bayesian mechanism design with submodular bidders.
In the classical survivable network design problem (SNDP), we are given an undirected graph G = (V, E) with costs on edges and a connectivity requirement k(s, t) for each pair of vertices. The goal is to find a minimum-cost subgraph H subset of G such that every pair (s, t) is connected by k(s, t) edge or (openly) vertex disjoint paths, abbreviated as EC-SNDP and VC-SNDP, respectively. The seminal result of Jain [FOCS'98, Combinatorica'01] gives a 2-approximation algorithm for EC-SNDP, and a decade later, an O(k(3) log n)-approximation algorithm for VC-SNDP, where k is the largest connectivity requirement, was discovered by Chuzhoy and Khanna [FOCS'09, Theory Comput.'12]. While there is a rich literature on point-to-point settings of SNDP, the viable case of connectivity between subsets is still relatively poorly understood. This article concerns the generalization of EC-SNDP into the subset-to-subset setting, namely Group EC-SNDP. We develop a framework, which yields the first non-trivial (true) approximation algorithm for Group EC-SNDP. Previously, only a bicriteria approximation algorithm is known for Group EC-SNDP [Chalermsook, Grandoni, and Laekhanukit, SODA'15], and a true approximation algorithm is known only for the single-source variant with connectivity requirement k(S, T) is an element of {0, 1, 2} [Gupta, Krishnaswamy, and Ravi, SODA'10; Khandekar, Kortsarz, and Nutov, FSTTCS'09 and Theor. Comput. Sci.'12]. On the negative side, in terms of the number of connectivity demands q, we give an Omega (q/log q)-hardness result for large k, complementing the previous inapproximability results, e.g., hardness in terms of k: k(1/5-epsilon)- hardness [Cheriyan et al., SODA'12; Laekhanukit, SODA'14; Chalermsook et al., SODA'15; Manurangsi, IPL'19]; hardness in terms of n: 2(log1-epsilon) (n)-hardness [Chalermsook et al., SODA'15].
