Joint Seminar on Theoretical Computer Science

Here is the list of joint seminar on theoretical computer science with Discrete and Computational Geometry Laboratory.

Computing Periods...

• February 27, 17h00, #3420
• Junhee Cho (KAIST)

Abstract: A period is the difference between the volumes of two semi-algebraic sets. Recent research has located their worst-case complexity in low levels of the Grzegorczyk Hierarchy. The present work introduces, analyzes, and evaluates three rigorous algorithms for rigorously computing periods: a deterministic, a randomized, and a 'transcendental' one.

(Joint work with Sewon Park, to be presented at WALCOM 2018)

On computability and complexity of finding solutions of linear hyperbolic systems of PDEs

• December 12, 16h30, #3444
• Svetlana Selivanova (Sobolev Institute, Novosibirsk)

Abstract: We discuss possibilities of application of methods of numerical analysis and computer algebra to investigate computability and complexity of finding solution operators of linear hyperbolic systems of PDEs. Computability is considered in the sense of the Weirauch’s TTE approach. We also report on our recent results in this area.

Probably Approximately Correct Learning

• Nov 23, 12h00
• E3-1 #2445
• Donghyun Lim (KAIST)

Abstract: PAC learning is a theoretical framework for the rigorous mathematical analysis of machine learning proposed in 1984 by Leslie Valiant. We motivate the approach, introduce the basic concept(s), survey the most important theorem(s), sketch an example proof, and present an example application.

Unpredictable random number generator based on thread scheduler

• Oct 26, 12h00
• E3-1 #2445
• Hyun Woo Lee (Hongik University)

Abstract: Adrian, Radu, and Sebastian suggested the software strategy to implement Unpredictable random number generator (URNG) based on the functionality of the operating system’s thread scheduler (2008). Based on their work, I make more simple but powerful URNG which produce the unpredictable random bits. By the NIST statistical test, I can check c++ implementation of this generator can make high quality random number faster than Adrian and 2 others’ strategy.

Formal Verification in Imperative Multivalued Programming over Continuous Data Types

• Sep 29, 12h00
• E3-1 #3444
• Sewon Park (KAIST)

Abstract: Inspired and guided by the iRRAM C++ library (Müller 2001), we formally specify a programming language for the paradigm of EXACT REAL COMPUTATION: reliably operating on encapsulated CONTINUOUS data types such as (not necessarily algebraic) real numbers — imperatively and exactly (no rounding errors) with primitives computable in the sense of Recursive Analysis and a necessarily modified multivalued=non-extensional semantics of tests. We then propose a complete logical system over two types, integers and real numbers, for rigorous correctness proofs of such algorithms. We extend the rules of Hoare Logic to support the formal derivation of such proofs, and have them verified in the Coq Proof Assistant. Our approach is exemplified with three simple numerical example problems: integer rounding, solving systems of linear equations, and continuous root finding.

(joint work with Gyesik Lee, Norbert Müller, Eike Neumann, Sewon Park, and Norbert Preining)

Undirected Reachability in LOGSPACE

• Sep. 7, 14h30
• E3-1 #4420
• Ivan Koswara (KAIST)

Abstract: We report the result of Reingold (2004) to decide undirected s-t connectivity in deterministic logarithmic space. We also report results about universal traversal sequences, which formed an important step towards solving the deterministic space complexity of undirected s-t connectivity.

Space-Complexity of Reachability

• August 17, 10h00
• E3-1 #2452
• Ivan Koswara (KAIST)

Abstract: We report on work by Nisan, Szemeredy, and Wigderson (1992) deciding undirected graph reachability in deterministic space O(log^{1.5} n); and on Trifonov's 2005 improvement to space O(log(n)*loglog(n)).

Surface Realization using FB-LTAG and Possible Issues on Implementation

• August 14, 15h00
• E3-1 #3445
• Seung-Woo Schin (KAIST)

Abstract: This talk will cover one of the surface realization technique using Feature Structure Based Lexicalized Tree Adjoining Grammar(FB-LTAG), suggested by [1]. After that, talk will cover possible issues in applying [1] to Basbalo framework. Firstly, FB-LTAG formalism will be introduced. FB-LTAG will serve as a grammar 'template' that contains both syntactic and semantic information. Than grammar extraction - which is denoted by FB-LTAG - algorithm from a preprocessed natural language will be suggested. Part-of-speech(POS) parse tree of a sentence and RDF Triples that contains semantic of a sentence will be used as a preprocessed data for a natural language sentence. Whole algorithm is suggested in [2].

In actual implementation of the framework, few issues need to be resolved.

1) Sentence preprocessing

On sentence preprocessing, generation of RDF triple is necessary. For now, Basbalo framework does not have ontology dedicated for baseball, which makes it impossible to generate RDF triple data. Therefore, comprehensive ontology implementation is necessary.

2) Language constraint

According to [3,4], linguistic issues can be addressed upon actual grammar extraction of Korean Language. Such constraint is mainly due to morphological difference between Korean language and English language.

3) Grammar abstractness vs Grammar scalability

Extracted grammar on [3,5] is too abstract, which is expected to increase difficulty of actual NLG process; if template semantics are too abstract, than appropriate template searching for a given semantic will be another issue. Therefore, finding the golden mean between scalabiltiy and usability will be key operation in later generation process.

[1] Claire Gardent. “Syntax and Data-to-Text Generation”. 2014.

[2] Bikash Gyawali. “Surface Realisation from Knowledge Bases”. 2016.

[3] Chung-hye Han, Juntae Yoon, Nari Kim and Martha Palmer. “A Feature-Based Lexicalized Tree Adjoining Grammar for Korean”. 2000.

[4] 이강천, 서정연. “의미 중심어에 기반한 한국어 문장 생성 시스템”. 1998.

[5] Sanghoun Song, Jong-Bok Kim, Francis Bond, Jaehyung Yang. “Development of the Korean Resource Grammar: Towards Grammar Customization”. 2010.

• August 3, 16h30
• E3-1 #2452
• Pieter Collins (Maastricht University)

Abstract: Many years ago, I was started work on a software package called Ariadne for verification of hybrid dynamic systems. This is a very hard problem, involving real numbers, functions and sets, nonlinear algebraic and differential equations, constraint satisfyability, and discontinuous behaviour, every calculation needs to be done rigorously for the result to be trustworthy. We would ideally even want to rigorously prove that our software is correct! The tool is therefore based on Computable Analysis to achieve clean syntax and semantics, with generic Interfaces for different Types leading allowing for various efficient implementations of Rigorous Numerical Algorithms.

I'll start by giving an overview of exact effective computational Real arithmetic, starting with a simple theoretical approach, and then showing how we implement these into code. I'll cover Ariadne's basic conceptualisation, such as Effective, Validated and Approximate objects, Symbolic, Bounds and Ball representations the Reals based on Dyadic and Floating-point numbers, and Accuracy, Effort, Precision, and Degree parameters. I will then show the Real number module in use. I'll then explain some of the more advanced features, such as the Functional calculus based on Taylor Polynomial Models, and finally give some examples of hybrid system verification in practice. Throughout the talk I will demonstrate features of Ariadne, both in C++ and the Python interpreter.

Finally, I will give some directions for further work, both within the Ariadne framework itself, and in the broader context of rigorous computational mathematics.

Hopefully, after this talk you will be motivated to try Ariadne yourselves to solve some problems, and maybe even contribute to it's development!

Online Resource Leasing

• May 2+4, 16h00-17h30
• E11 #309
• Friedhelm Meyer auf der Heide (Universität Paderborn)

Abstract: Decisions regarding which resources to acquire in order to provide services comprise the core of many optimization problems. Classical problems which fall into this category of problems are for example Facility Location, Steiner Tree, and Set Cover, as well as several scheduling problems. Such problems have been widely studied in both o?ine and online settings. Traditionally, the decisions are considered to be ?nal: we buy the resources. Once a resource is bought, it can be used any time in the future without inducing further costs. Inspired by the Cloud Computing market, we consider the leasing variants of the above problems: Resources are not bought, but leased for a given time interval; the cost for a lease typically grows with the length of the interval, but the cost per time unit decreases with this length. Such a model for leasing was introduced by Meyerson as the parking permit problem. In the lectures, I will present online algorithms for several resource leasing problems. Technically, our algorithmic approach is mostly based on an online variant of primal-dual approximation algorithms.

Algorithmic Foundations of Swarm Robotics

• April 25+27, 16h00-17h30
• E11 #309
• Friedhelm Meyer auf der Heide (Universität Paderborn)

Abstract: Swarm robotics considers large swarms of relatively simple mobile robots deployed to some 2- or 3-dimensional area. These robots have very limited sensor capabilities; typically they can only observe aspects of their local environment. The objective of swarm robotics is to understand which global behavior of a swarm is induced by local strategies, simultaneously executed by the individual robots. Typically, the decisions of the individual robots are based on local information only. In these lectures, I look at simple models of swarms of identical, anonymous robots: they are points in the plane and 'see' only their neighbors, i.e. the robots within distance one. I will focus on distributed local strategies of such swarms that result in formations like 'gathering in one point' or 'forming a line'. I will present several strategies for such formation problems, both in discrete and continuous time models, and show upper and lower bounds for their runtime and energy consumption.

On Verified Real Computation

• April 21, 12h00-13h30
• E3-1 #3420
• Sewon Park (KAIST)

Abstract: While Numerical Engineering often focuses on the raw performance of hardware FLOATs and heuristical “recipes” for most/“practical” instances, mission-critical applications and Computer-Assisted Proofs in Pure Mathematics require guaranteed correctness in all conceivable cases. Exact Real Computation is the paradigm of imperative programming over continuous abstract data types with (necessarily) modified, namely multivalued, semantics of tests. We (i) approach the problem of formal verification for such algorithms; and we (ii) devise, implement, and empirically evaluate three (variants of) algorithms for diagonalizing (i.e. computing a spectral decomposition of) possibly degenerate Hermitian matrices.

Bi-Topological Spaces and the Continuity Problem

• April 17, 16h00-17h30
• E6-1 #1409
• Dieter Spreen (Universität Siegen)

Abstract: The continuity problem is the question when effective (or Markov computable) maps between effectively given topological spaces are effectively continuous. It will be shown that this is always the case if the the range of the map is effectively bi-regular. As will be shown, such spaces appear quite naturally in the context of the problem.

Putting your coin collection on a shelf

• April 3, 16h00-17h30
• E6-1 #1409
• Otfried Cheong (KAIST)

Abstract: Imagine you want to present your collection of n coins on a shelf, taking as little space as possible – how should you arrange the coins?

More precisely, we are given n circular disks of different radii, and we want to place them in the plane so that they touch the x-axis from above, such that no two disks overlap. The goal is to minimize the length of the range from the leftmost point on a disk to the rightmost point on a disk.

On this seemingly innocent problem we will meet a wide range of algorithmic concepts: An efficient algorithm for a special case, an NP-hardness proof, an approximation algorithm with a guaranteed approximation factor, APX-hardness, and a quasi-polynomial time approximation scheme.

Reliable Degenerate Matrix Diagonalization

• March 6, 13h00-14h30
• E3-1 #2452
• Sewon Park (KAIST)

Abstract: We consider the diagonalization of real symmetric square matrices with (not necessarily algebraic entries and) particular emphasis on the degenerate case: In general ill-posed and in fact provably uncomputable a problem, Recursive Analysis [Ziegler&Brattka'04] has established that some orthonormal basis of eigenvectors is computable in the sense of output approximation up to any desired precision - provided that, in addition to approximations to the d*(d+1)/2 matrix' entires, its number k of DISTINCT eigenvalues is known/provided. The present work explores the practical impact and quantitative efficiency of this qualitative and implicit result: We devise, combine, implement, evaluate, and compare four variants of rigorous and total algorithms guaranteed to (i) extract the coefficients of the matrix' characteristic polynomial, (ii) refine root enclosures of the latter using Pellet's Predicate until separating the $k$ disjoint clusters to thus derive the individual eigenvalues' multiplicities d[j] for 0<j⇐k, (iii) employ (some combination of) Trisection, Newton and/or Gräffe Iterations to improve said real root approximations to the precision required to finally (iv) determine an orthonormal base of eigenvectors to these eigenvalues. Algorithms (ii) and (iii) are based on, vary, and extend a recent series of contributions by Sagraloff, Sharma, Yap et al. (2013-2016), (iv) on own work (2016) using a variant of Gaussian Elimination that avoids total tests for real equality as these are known equivalent to the (complement of the) Halting Problem.

Our implementation builds on the C++ library iRRAM, providing an abstract data type REAL for rapid numerical prototyping with exact arithmetic and a subtly modified yet sound semantics of comparisons. Correctness is asserted by recovering the random eigenvector bases to a family or deliberately degenerate artificial test matrices; and efficiency is evaluated with respect to the three parameters output precision, matrix dimension, and eigenvalue separation. It confirms that the sophisticated combined algorithm of Sagraloff, Sharma, Yap et al. (2013-2016) is indeed practical and asymptotically outperforms the two simpler variants - but can in turn be improved by employing trisection for medium precision.

Computing statistical long-term properties of dynamical systems

• February 28, 18h00-19h00
• E3-1 #2452
• Holger Thies (The University of Tokyo)

Abstract: In this talk, we give an overview of some recent results by Braverman, Grigo and Rojas on the computability and complexity of long-term properties of dynamical systems. Dynamical systems are used to model a large number of processes in nature whose state evolves over time. Important questions deal with the long-term behavior of such systems when the time approaches infinity. We want to discuss computability and computational complexity of such questions in the sense of arbitrary precise approximations as studied in the field of computable analysis. While simulating such a system for bounded time is usually computable, long term properties often can not be determined in a computable way. Galatolo, Hoyrup and Rojas investigated statistical properties of discrete-time dynamical systems described by invariant measures. They show that a computable dynamic system does not necessarily have a computable invariant measure. On the other hand, Braverman, Grigo and Rojas could show that introducing a small amount of noise renders the system computable. We present some of their results and introduce the tools necessary to understand them.

Analyzing Markov Chains using Belief Propagation

• December 16, 15h00-16h00
• E6-1 #1409
• Eric Vigoda (Georgia Institute of Technology)

For counting weighted independent sets weighted by a parameter λ (known as the hard-core model) there is a beautiful connection between statistical physics phase transitions on infinite, regular trees and the computational complexity of approximate counting on graphs of maximum degree D. For λ below the critical point there is an elegant algorithm devised by Weitz (2006). The drawback of his algorithm is that the running time is exponential in log D. In this talk we’ll describe recent work which shows O(n log n) mixing time of the single-site Markov chain when the girth>6 and D is at least a sufficiently large constant. Our proof utilizes BP (belief propagation) to design a distance function in our coupling analysis. This is joint work with C. Efthymiou, T. Hayes, D. Stefankovic, and Y. Yin which appeared in FOCS ’16.

Paper review: Construction of real algebraic numbers in Coq

• December 9, 11h00-12h00
• E3-1 #2452
• Gyesik Lee (Hankyong National University)

In this talk, we will review the following paper: Cyril Cohen, "Construction of real algebraic numbers in Coq", February 18, 2012.

Abstract: This paper shows a construction in Coq of the set of real algebraic numbers, together with a formal proof that this set has a structure of discrete archimedian real closed field. This construction hence implements an interface of real closed field. Instances of such an interface immediately enjoy quantifier elimination thanks to a previous work. This work also intends to be a basis for the construction of complex algebraic numbers and to be a reference implementation for the certification of numerous algorithms relying on algebraic numbers in computer algebra.

Introduction to Coq

• October 5, 16h00-18h00
• E3-1 #2452
• Sunyoung Kim (Yonsei University)

Abstract : In this talk, we introduce a proof assistant Coq, which is based on the Calculus of Inductive Constructions (CIC). Since CIC is a variant of the calculus of construction (CoC : a higher-order typed lambda calculus), we briefly consider type theory and whose central theme Curry-Howard isomorphism. We will give easy exercises that can be proved by using Coq. The C-CoRN library for Coq takes an approach different from the standard library of Coq. At last, we discuss the real numbers in Coq.

Another New Foundation: A Theory with Combined Concepts from Set Theory, Type Theory and Lesniewski's Mereology

• September 30, 12h30-14h00
• E3-1 #2452
• Jin Hoo Lee (KAIST)

We introduce a new theory which encompasses concepts and ideas from set theory, type theory, and Lesniewski's mereology and describes its possibility as an alternative foundation for mathematics. In the introduction section I will introduce motives for development of the theory and some remarks on the methods of presentation. Axioms of the theory and their philosophical background and justi cation on the basis of intuitive view are discussed next. Discussed after are realizations of mathematical concepts such as N, Z, Q, R, C, etc. Then this paper concludes with comparisons between the theory and ZFC and its mathematical limitations.

Root Clustering Problem of Analytic functions

• September 26, 12h00-13h00
• E3-1 #2452
• Sewon Park (KAIST)

Well-known Algorithms for root isolating problem consider a polynomial function which has simple roots only. Recent work of Chee Yap et al., 2013, devised an algorithm which enables to isolate (cluster) roots with multiplicities of any analytic function. This talk will review the work of Chee Yap et al., and discuss about an implementation and verification of the suggested algorithm.

Analytic Functions - From Real Complexity Theory to Implementation

• September 8, 14h30-15h45
• E3-1 #3445
• Holger Thies (University of Tokyo)

We consider the problem of solving systems of ordinary differential equations in exact real arithmetic, i.e., in the sense of arbitrarily precise numerical computations. It is known from real complexity theory that this problem is PSPACE-hard in the general case. However, when restricting the right hand side functions of the system to be not only polynomial time computable but also analytic, the solutions will again be polynomial time computable and analytic. By carefully choosing the representation, this result can even be turned into uniform algorithms on analytic functions. The talk consists of two parts. First we explore analytic functions from the view point of real complexity theory and give running time and space bounds for various operations. We then show how to turn those theorems into algorithms and use them for practical implementations in the C++ programming language based on the iRRAM library. To that end, we also give a representation for multidimensional analytic functions in terms of an abstract data type and an implementation of such a type. We further give implementations of several different algorithms to solve the ODE problem and compare their running times.

Topological View on Computational Shape Optimization

• August 11, 14h00-15h30
• E3-1 #2452
• Dongseong Seon and Chansu Park (both KAIST interns from SNU)

By the sometimes so-called MAIN THEOREM of Recursive Analysis, a computable function must necessarily be continuous. We investigate this condition for example primitives in Shape Optimization: volume, perimeter, and convexity, considered as real-valued objective/constraint functionals on various classes of compact sets equipped with the Hausdorff metric.

Computational Complexity of N-Body Problem

• August 1, 14h00-15h30
• E3-1 #2452
• Seungwoo Schin (KAIST)

N-body problem is classical problem in physics. In this talk, error bound of stepwise simulation of n-body problem will be discussed. As a side-result of error bound discussion, it can be shown that n-body reachability problem is PSPACE. Then, to show PSPACE-hardness, reduction from other problems that are known to be PSPACE-hard will be given. To be specific, following problems will be discussed; 1) Ray-tracing problem with rational coefficient reflecting obstacles(and for a brainteaser, equivalent problem in game of go will be discussed, which it's equivalence is very straightforward with the given problem), 2) 1-body reachability problem with immobile rectangular obstacles, 3) 1-body reachability problem with uniformly distributed charge plate obstacles, while both problems are discussed with restriction to the impact position.

Holographic Algorithms

• June 22, 11h30-13h30
• E3-1 #2452
• Iwan Koswara (KAIST)

In computer science, a holographic algorithm is an algorithm that uses a holographic reduction. A holographic reduction is a constant-time reduction that maps solution fragments many-to-many such that the sum of the solution fragments remains unchanged. These concepts were introduced by Leslie Valiant, who called them holographic because “their effect can be viewed as that of producing interference patterns among the solution fragments”. The algorithms are unrelated to laser holography, except metaphorically. Their power comes from the mutual cancellation of many contributions to a sum, analogous to the interference patterns in a hologram. Holographic algorithms have been used to find polynomial-time solutions to problems without such previously known solutions for special cases of satisfiability, vertex cover, and other graph problems. They have received notable coverage due to speculation that they are relevant to the P versus NP problem and their impact on computational complexity theory. Although some of the general problems are #P-hard problems, the special cases solved are not themselves #P-hard, and thus do not prove FP = #P. Holographic algorithms have some similarities with quantum computation, but are completely classical.

The Ford-Fulkerson Algorithm and its Analysis

• June 1, 14h30-16h00
• E3-1 #2452
• 장문수 (KAIST)

Algorithms for computing the 2D convex hull

• May 27, 14h30-16h00
• E3-1 #2452
• Imran Fareed (KAIST)

Algorithms for Parallel Computers

• May 26, 16h30-18h00
• E3-1 #2452
• Dongkyu Lee (KAIST)

Obstructing Visibilities with One Obstacle

• May 25, 12h00-14h00
• E3-1 #2452
• Jiwon Park (KAIST)

An obstacle representation of a graph G is a drawing of G in the plane with polygons called obstacles; two points are adjacent iff the straight line segment connecting them does not intersect any obstacles. Obstacle number of a graph is the smallest number of obstacles which allows an obstacle representation of the graph. Even a class of graphs of obstacle number 1 is not known completely. There is a nice characterization for graphs which have a representation with 1 convex obstacle: non-double covering circular arc graphs. Also it is known that every outerplanar graph has a representation with 1 outside obstacle. And as far as I know, they are all results about graphs of obstacle number 1.

In this talk, the following new results are presented:

1. A smallest graph of obstacle number 2. It has 8 vertices and it is tight. (the smallest graph of obstacle number 2 known so far had 10 vertices)
2. Every graph of circumference at most 6 has an outside obstacle representation.
3. A class of graphs with an outside obstacle and a a class of graphs without outside obstacle are different. (it was one of main questions on the obstacle number of graphs)

The Knuth-Morris-Pratt (KMP) Algorithm for String Matching

• May 18, 16h30-18h00
• E3-1 #2452
• 김영석 (Tony) from KAIST's School of Computing

Towards Capturing Order-Independent P

• May 11, 16h00-17h30
• E3-1 #3445
• Neil Immerman (University of Massachusetts)

In Descriptive Complexity we characterize the complexity of decision problems by how rich a logical language is needed to describe the problem. Important complexity classes have natural logical characterizations, for example NP is the set of problems expressible in second order existential logic (NP =SOE) and P is the set of problems expressible in first order logic, plus a fixed point operator (P = FO(FP)).

The latter characterization is over ordered graphs, i.e. the vertex set is a linearly ordered set. This is appropriate for computational problems because all inputs to a computer are ordered sequences of bits. Any ordering will do; we are interested in the order-independent properties of graphs. The search for order-independent P is closely tied to the complexity of graph isomorphism. I will explain these concepts and the current effort to capture order-independent P.

Escape probabilities and stationary distribution of metastable Markov chains: theory and computation

• April.15 14h00-16h00
• E3-1 #4443

Metastability is often an obstacle to efficient computation or simulation of average or typical quantities of stochastic dynamical systems. In particular when there is no reversibility, and thus potential theory is not available, few methods exist. In this talk I will argue that escape probabilities are the right object to study in this case, and will show how they determine the metastable dynamics of finite Markov chains. This will lead to an efficient way of computing both the dynamics and the stationary distribution of metastable Markov chains.

Computational complexity theory for spaces of integrable functions

• Apr.15 10h30-12h00
• E3-1 #4443
• Florian Steinberg (TU Darmstadt and University of Tokyo)

The framework of second order representations was introduced by Kawamura and Cook in 2010 and provides a rigorous notion of computation over continuous structures. It also provides a notion of time and space restricted computation. Choosing a representation means to specify what information a program computing an element of the structure has to provide. We relate the existence of a reasonable choice of information on a compact metric space to a purely metric property of the space: The metric entropy of a compact metric space measures fast the number of balls needed to cover the space grows with the radius of the balls decreasing. We show that the optimal running time of the metric is inherently connected to the metric entropy. These results are applied to show optimality of some concrete representations of function spaces

Automatic Design of Casts for 3D Printing

• Mar.11 12h30-14h30
• E3-1 #2452
• Jaewoong Han (U-Waterloo and KAIST)

The modern civilization evolved with the series of industrial revolutions. According to Jeremy Rifkin, 3-D printing is the third industrial revolution that minimizes the cost of building and fastens the process of designing. In addition, easier access to a private 3-D printer will personally customize products by the user and for the user.

The 3-D printers are not affordable for everyone yet, but in near future, people will design their own products with their own 3-D printer at home. As it is a new technology, there is a lack of software applications related to 3-D printing in the market. An user-friendly program that designs and builds a set of moulds for the user’s own product is in demand.

There are a number of complications when using a 3-D printer and designing a mould. It is critical to clean and maintain a 3-D printer properly to ensure the quality of the printed parts. Many techniques apply in designing a mould to reduce the material and speed up the process of printing.

A complex convex octahedron is chosen as an input product by the user. The software application will be programmed to create eight pieces of mould for the polyhedron. Using OpenSCAD, an open-sourced software application for creating 3-D computer-aided designs, the program will locate six vertices, create a bounding box, implement existing library to convert vertices to normal vectors of faces and vice versa, calculate cross products of vectors to form cutting planes, and then divide the bounding box into eight parts. Moreover, further improvements will be made, including increasing the size of the bounding box, adding a sprue for pouring material, attaching the connecting section for each piece of the mould, and upgrading the algorithm of the program to deal with more complex geometry.

Algebraic Specification and Verification - an Introduction to CafeOBJ

• Jan.25 10h30-12h00 and 16h00-17h30, Jan.26 10h30-12h00
• E3-1 #3445
• Norbert Preining (JAIST)

Ensuring correctness of complex systems like computer programs or communication protocols is gaining ever increasing importance. For correctness it does not suffice to consider the finished system, but correctness already on the level of specification is necessary, that is, before the actual implementation starts. To this aim, algebraic specification and verification languages have been conceived. They are aiming at a mathematically correct description of the properties and behavior of the systems under discussion, and in addition often allow to prove (verify) correctness within the same system.

This course will give an introduction to algebraic specification, its history, logic roots, and actuality with respect to current developments. Paired with the theoretical background we give an introduction to CafeOBJ, a programming language that allows both specification and verification to be carried out together. The course should enable participants to understand the theoretical background of algebraic specification, as well as enable them to read and write basic specifications in CafeOBJ.

Shortcuts for the Circle

• Dec 10, 12h30
• E3-1 #2450
• Otfried Cheong (KAIST) (joint work with Mark de Berg, Sang Won Bae, Joachim Gudmundsson, and Christos Levcopoulos)

Let $C$ be the unit circle in $\mathbb{R}^2$. We can view $C$ as a plane graph whose vertices are all the points on $C$, and the distance between any two points on $C$ is the length of the smaller arc between them. We consider a graph augmentation problem on $C$, where we want to place $k \ge 1$ shortcuts on $C$ such that the diameter of the resulting graph is minimized. We analyze for each $k$ with $1 \le k \le 7$ what the optimal set of shortcuts is. Interestingly, the minimum diameter one can obtain is not a strictly decreasing function of $k$. For example, with seven shortcuts one cannot obtain a smaller diameter than with six shortcuts. Finally, we prove that the optimal diameter is $2 + \Theta (1/k^\frac{2}{3})$ for any $k$.

Worst-Case vs. Average-Case Bit-Complexity Theory of Real Functions

• Dec 3, 14h30
• N1 #111
• Martin Ziegler (KAIST)

While concepts and tools from Theoretical Computer Science are regularly applied to, and significantly support, software development for discrete problems, Numerical Engineering largely employs recipes and methods whose correctness and efficiency is demonstrated empirically. We advertise Real Complexity Theory: a resource-oriented foundation to rigorous computations over continuous universes such as real numbers, vectors, sequences, continuous functions, and Euclidean subsets: in the bit-model by approximation up to given absolute error. We review the underlying notions and some illustrative results – regarding worst-case complexity theory; to then introduce, and initiate the study of, average-case bit-complexity theory over the reals: Like in the discrete case a first, naive notion of polynomial average runtime turns out to lack robustness and is thus refined. Standard examples of explicit continuous functions with increasingly high worst-case complexity are shown to be in fact easy in the mean; while a further example is constructed with both worst and average complexity exponential: for topological/metric reasons, i.e., oracles do not help.

Well-Separated Pair Decomposition and the Fast Multipole Method

• Nov 26, 12h30
• E3-1 #2450

The N-body problem cannot be solved analytically for N>2 and hence is generally approached numerically. Naive algorithms incur cost quadratic in N; and we report on the state-of-the-art achieving subquadratic runtime by means of approximation: the Fast Multipole Method, said to be among the top ten algorithms of the 20th century. We present a rigorous worst-case performance analysis, based on techniques from computational geometry and in terms of bit cost.

Symmetric Difference is a Metric for Convex Shapes Modulo Homothety

• Nov 17, 13h00
• E3-1 #3420
• Ji-Won Park (KAIST)

Symmetric difference can be used to measure similarity between two shapes. In this talk, similarity up to homothety, which is a combination of translations and scaling, is concerned and there is a recent result of Yon et al. about it. However, their definition is not symmetric and thus not metric. We introduce a variant of symmetric difference whic his a metric for convex shapes modulo homothety (so two convex shapes are regarded the same iff one is a homothety of the other) and provide a proof.

• Nov 3, 12h45
• E3-1 #3420