Keiichi Watanabe
A Software Engineer at Google
Research Areas
Authored Publications
Sort By
Preview abstract
Regular-polygon geometry is tightly linked to cyclotomic arithmetic: Poonen and Rubinstein’s treatment of three-diagonal concurrence, for example, turns a geometric incidence condition into a short vanishing sum of roots of unity.
We prove an analogous rigidity result for areas. Two congruent crossing diagonals divide a regular n-gon into four regions. For the four regions cut out by the two congruent crossing diagonals V0Vm and VkVn−m+k of a regular n-gon, we completely classify, for all parameters (n, k, m), which sums of the normalized areas a0, . . . , a3 are rational. The classification has a sharp finite–infinite contrast: a0 is rational in only five configurations, whereas the rational cases for a2 and adjacent two-region sums form infinite families. Rationality is delicately sensitive to the parameters: for the configuration (14, 3, 5), no nontrivial subset sum is rational, while the neighboring cut (14, 4, 5) gives a2 = 5/7.
The proof reduces each rationality condition to trigonometric relations at rational multiples of π and combines cyclotomic norm arguments with the classification theorems of Conway–Jones and Poonen–Rubinstein.
View details
Reduction from Branching-time Property Verification of Higher-Order Programs to HFL Validity Checking
Hiroki Oshikawa
Naoki Kobayashi
Takeshi Tsukada
43rd International Symposium on Mathematical Foundations of Computer Science (2019)
Preview abstract
Various methods have recently been proposed for temporal property verification of higher-order programs. In those methods, however, either temporal properties were limited to linear-time ones, or target programs were limited to finite-data programs. In this paper, we extend Kobayashi et al.’s recent method for verification of linear-time temporal properties based on HFLz model checking, to deal with branching-time properties. We formalize branching-time property verification problems as an extension of HORS model checking called HORSz model checking, present a sound and complete reduction to validity checking of (modal-free) HFLz formulas, and prove its correctness. The correctness of the reduction subsumes the decidability of HORS model checking. The HFLz formula obtained by the reduction from a HORSz model checking problem can be considered a kind of verification condition for the orignal model checking problem. We also discuss interactive and automated methods for discharging the verification condition.
View details
