-
Enriched Presheaf Model of Quantum FPC
Authors:
Takeshi Tsukada,
Kazuyuki Asada
Abstract:
Selinger gave a superoperator model of a first-order quantum programming language and proved that it is fully definable and hence fully abstract. This paper proposes an extension of the superoperator model to higher-order programs based on modules over superoperators or, equivalently, enriched presheaves over the category of superoperators. The enriched presheaf category can be easily proved to be…
▽ More
Selinger gave a superoperator model of a first-order quantum programming language and proved that it is fully definable and hence fully abstract. This paper proposes an extension of the superoperator model to higher-order programs based on modules over superoperators or, equivalently, enriched presheaves over the category of superoperators. The enriched presheaf category can be easily proved to be a model of intuitionistic linear logic with cofree exponential, from which one can cave out a model of classical linear logic by a kind of bi-orthogonality construction. Although the structures of an enriched presheaf category are usually rather complex, a morphism in the classical model can be expressed simply as a matrix of completely positive maps. The model inherits many desirable properties from the superoperator model. A conceptually interesting property is that our model has only a state whose "total probability" is bounded by 1, i.e. does not have a state where true and false each occur with probability 2/3. Another convenient property inherited from the superoperator model is a $ω$CPO-enrichment. Remarkably, our model has a sufficient structure to interpret arbitrary recursive types by the standard domain theoretic technique. We introduce Quantum FPC, a quantum $λ$-calculus with recursive types, and prove that our model is a fully abstract model of Quantum FPC.
△ Less
Submitted 6 November, 2023;
originally announced November 2023.
-
Neutron Tagging following Atmospheric Neutrino Events in a Water Cherenkov Detector
Authors:
K. Abe,
Y. Haga,
Y. Hayato,
K. Hiraide,
K. Ieki,
M. Ikeda,
S. Imaizumi,
K. Iyogi,
J. Kameda,
Y. Kanemura,
Y. Kataoka,
Y. Kato,
Y. Kishimoto,
S. Miki,
S. Mine,
M. Miura,
T. Mochizuki,
S. Moriyama,
Y. Nagao,
M. Nakahata,
T. Nakajima,
Y. Nakano,
S. Nakayama,
T. Okada,
K. Okamoto
, et al. (281 additional authors not shown)
Abstract:
We present the development of neutron-tagging techniques in Super-Kamiokande IV using a neural network analysis. The detection efficiency of neutron capture on hydrogen is estimated to be 26%, with a mis-tag rate of 0.016 per neutrino event. The uncertainty of the tagging efficiency is estimated to be 9.0%. Measurement of the tagging efficiency with data from an Americium-Beryllium calibration agr…
▽ More
We present the development of neutron-tagging techniques in Super-Kamiokande IV using a neural network analysis. The detection efficiency of neutron capture on hydrogen is estimated to be 26%, with a mis-tag rate of 0.016 per neutrino event. The uncertainty of the tagging efficiency is estimated to be 9.0%. Measurement of the tagging efficiency with data from an Americium-Beryllium calibration agrees with this value within 10%. The tagging procedure was performed on 3,244.4 days of SK-IV atmospheric neutrino data, identifying 18,091 neutrons in 26,473 neutrino events. The fitted neutron capture lifetime was measured as 218 \pm 9 μs.
△ Less
Submitted 20 September, 2022; v1 submitted 18 September, 2022;
originally announced September 2022.
-
Linear-Algebraic Models of Linear Logic as Categories of Modules over Sigma-Semirings
Authors:
Takeshi Tsukada,
Kazuyuki Asada
Abstract:
A number of models of linear logic are based on or closely related to linear algebra, in the sense that morphisms are "matrices" over appropriate coefficient sets. Examples include models based on coherence spaces, finiteness spaces and probabilistic coherence spaces, as well as the relational and weighted relational models. This paper introduces a unified framework based on module theory, making…
▽ More
A number of models of linear logic are based on or closely related to linear algebra, in the sense that morphisms are "matrices" over appropriate coefficient sets. Examples include models based on coherence spaces, finiteness spaces and probabilistic coherence spaces, as well as the relational and weighted relational models. This paper introduces a unified framework based on module theory, making the linear algebraic aspect of the above models more explicit. Specifically we consider modules over Sigma-semirings $R$, which are ring-like structures with partially-defined countable sums, and show that morphisms in the above models are actually $R$-linear maps in the standard algebraic sense for appropriate $R$. An advantage of our algebraic treatment is that the category of $R$-modules is locally presentable, from which it easily follows that this category becomes a model of intuitionistic linear logic with the cofree exponential. We then discuss constructions of classical models and show that the above-mentioned models are examples of our constructions.
△ Less
Submitted 22 April, 2022;
originally announced April 2022.
-
Automatic HFL(Z) Validity Checking for Program Verification
Authors:
Naoki Kobayashi,
Kento Tanahashi,
Ryosuke Sato,
Takeshi Tsukada
Abstract:
We propose an automated method for checking the validity of a formula of HFL(Z), a higher-order logic with fixpoint operators and integers. Combined with Kobayashi et al.'s reduction from higher-order program verification to HFL(Z) validity checking, our method yields a fully automated, uniform verification method for arbitrary temporal properties of higher-order functional programs expressible in…
▽ More
We propose an automated method for checking the validity of a formula of HFL(Z), a higher-order logic with fixpoint operators and integers. Combined with Kobayashi et al.'s reduction from higher-order program verification to HFL(Z) validity checking, our method yields a fully automated, uniform verification method for arbitrary temporal properties of higher-order functional programs expressible in the modal mu-calculus, including termination, non-termination, fair termination, fair non-termination, and also branching-time properties. We have implemented our method and obtained promising experimental results.
△ Less
Submitted 8 December, 2022; v1 submitted 14 March, 2022;
originally announced March 2022.
-
Software Model-Checking as Cyclic-Proof Search
Authors:
Takeshi Tsukada,
Hiroshi Unno
Abstract:
This paper shows that a variety of software model-checking algorithms can be seen as proof-search strategies for a non-standard proof system, known as a cyclic proof system. Our use of the cyclic proof system as a logical foundation of software model checking enables us to compare different algorithms, to reconstruct well-known algorithms from a few simple principles, and to obtain soundness proof…
▽ More
This paper shows that a variety of software model-checking algorithms can be seen as proof-search strategies for a non-standard proof system, known as a cyclic proof system. Our use of the cyclic proof system as a logical foundation of software model checking enables us to compare different algorithms, to reconstruct well-known algorithms from a few simple principles, and to obtain soundness proofs of algorithms for free. Among others, we show the significance of a heuristics based on a notion that we call maximal conservativity; this explains the cores of important algorithms such as property-directed reachability (PDR) and reveals a surprising connection to an efficient solver of games over infinite graphs that was not regarded as a kind of PDR.
△ Less
Submitted 10 November, 2021;
originally announced November 2021.
-
Termination Analysis for the $π$-Calculus by Reduction to Sequential Program Termination
Authors:
Tsubasa Shoshi,
Takuma Ishikawa,
Naoki Kobayashi,
Ken Sakayori,
Ryosuke Sato,
Takeshi Tsukada
Abstract:
We propose an automated method for proving termination of $π$-calculus processes, based on a reduction to termination of sequential programs: we translate a $π$-calculus process to a sequential program, so that the termination of the latter implies that of the former. We can then use an off-the-shelf termination verification tool to check termination of the sequential program. Our approach has bee…
▽ More
We propose an automated method for proving termination of $π$-calculus processes, based on a reduction to termination of sequential programs: we translate a $π$-calculus process to a sequential program, so that the termination of the latter implies that of the former. We can then use an off-the-shelf termination verification tool to check termination of the sequential program. Our approach has been partially inspired by Deng and Sangiorgi's termination analysis for the $π$-calculus, and checks that there is no infinite chain of communications on replicated input channels, by converting such a chain of communications to a chain of recursive function calls in the target sequential program. We have implemented an automated tool based on the proposed method and confirmed its effectiveness.
△ Less
Submitted 1 September, 2021;
originally announced September 2021.
-
Learning Heuristics for Template-based CEGIS of Loop Invariants with Reinforcement Learning
Authors:
Minchao Wu,
Takeshi Tsukada,
Hiroshi Unno,
Taro Sekiyama,
Kohei Suenaga
Abstract:
Loop-invariant synthesis is the basis of program verification. Due to the undecidability of the problem in general, a tool for invariant synthesis necessarily uses heuristics. Despite the common belief that the design of heuristics is vital for the performance of a synthesizer, heuristics are often engineered by their developers based on experience and intuition, sometimes in an \emph{ad-hoc} mann…
▽ More
Loop-invariant synthesis is the basis of program verification. Due to the undecidability of the problem in general, a tool for invariant synthesis necessarily uses heuristics. Despite the common belief that the design of heuristics is vital for the performance of a synthesizer, heuristics are often engineered by their developers based on experience and intuition, sometimes in an \emph{ad-hoc} manner. In this work, we propose an approach to systematically learning heuristics for template-based CounterExample-Guided Inductive Synthesis (CEGIS) with reinforcement learning. As a concrete example, we implement the approach on top of PCSat, which is an invariant synthesizer based on template-based CEGIS. Experiments show that PCSat guided by the heuristics learned by our framework not only outperforms existing state-of-the-art CEGIS-based solvers such as HoICE and the neural solver Code2Inv, but also has slight advantages over non-CEGIS-based solvers such as Eldarica and Spacer in linear Constrained Horn Clause (CHC) solving.
△ Less
Submitted 15 June, 2022; v1 submitted 16 July, 2021;
originally announced July 2021.
-
A Probabilistic Higher-order Fixpoint Logic
Authors:
Yo Mitani,
Naoki Kobayashi,
Takeshi Tsukada
Abstract:
We introduce PHFL, a probabilistic extension of higher-order fixpoint logic, which can also be regarded as a higher-order extension of probabilistic temporal logics such as PCTL and the $μ^p$-calculus. We show that PHFL is strictly more expressive than the $μ^p$-calculus, and that the PHFL model-checking problem for finite Markov chains is undecidable even for the $μ$-only, order-1 fragment of PHF…
▽ More
We introduce PHFL, a probabilistic extension of higher-order fixpoint logic, which can also be regarded as a higher-order extension of probabilistic temporal logics such as PCTL and the $μ^p$-calculus. We show that PHFL is strictly more expressive than the $μ^p$-calculus, and that the PHFL model-checking problem for finite Markov chains is undecidable even for the $μ$-only, order-1 fragment of PHFL. Furthermore the full PHFL is far more expressive: we give a translation from Lubarsky's $μ$-arithmetic to PHFL, which implies that PHFL model checking is $Π^1_1$-hard and $Σ^1_1$-hard. As a positive result, we characterize a decidable fragment of the PHFL model-checking problems using a novel type system.
△ Less
Submitted 1 December, 2021; v1 submitted 29 November, 2020;
originally announced November 2020.
-
A Cyclic Proof System for HFLN
Authors:
Mayuko Kori,
Takeshi Tsukada,
Naoki Kobayashi
Abstract:
A cyclic proof system allows us to perform inductive reasoning without explicit inductions. We propose a cyclic proof system for HFLN, which is a higher-order predicate logic with natural numbers and alternating fixed-points. Ours is the first cyclic proof system for a higher-order logic, to our knowledge. Due to the presence of higher-order predicates and alternating fixed-points, our cyclic proo…
▽ More
A cyclic proof system allows us to perform inductive reasoning without explicit inductions. We propose a cyclic proof system for HFLN, which is a higher-order predicate logic with natural numbers and alternating fixed-points. Ours is the first cyclic proof system for a higher-order logic, to our knowledge. Due to the presence of higher-order predicates and alternating fixed-points, our cyclic proof system requires a more delicate global condition on cyclic proofs than the original system of Brotherston and Simpson. We prove the decidability of checking the global condition and soundness of this system, and also prove a restricted form of standard completeness for an infinitary variant of our cyclic proof system. A potential application of our cyclic proof system is semi-automated verification of higher-order programs, based on Kobayashi et al.'s recent work on reductions from program verification to HFLN validity checking.
△ Less
Submitted 12 August, 2021; v1 submitted 28 October, 2020;
originally announced October 2020.
-
Signature Restriction for Polymorphic Algebraic Effects
Authors:
Taro Sekiyama,
Takeshi Tsukada,
Atsushi Igarashi
Abstract:
The naive combination of polymorphic effects and polymorphic type assignment has been well known to break type safety. Existing approaches to this problem are classified into two groups: one for restricting how effects are triggered and the other for restricting how they are implemented. This work explores a new approach to ensuring the safety of polymorphic effects in polymorphic type assignment.…
▽ More
The naive combination of polymorphic effects and polymorphic type assignment has been well known to break type safety. Existing approaches to this problem are classified into two groups: one for restricting how effects are triggered and the other for restricting how they are implemented. This work explores a new approach to ensuring the safety of polymorphic effects in polymorphic type assignment. A novelty of our work lies in finding a restriction on effect interfaces. To formalize our idea, we employ algebraic effects and handlers, where an effect interface is given by a set of operations coupled with type signatures. We propose signature restriction, a new notion to restrict the type signatures of operations, and show that signature restriction is sufficient to ensure type safety of an effectful language equipped with unrestricted polymorphic type assignment. We also develop a type-and-effect system to enable the use of both operations that satisfy and do not satisfy the signature restriction in a single program.
△ Less
Submitted 29 August, 2020; v1 submitted 18 March, 2020;
originally announced March 2020.
-
RustHorn: CHC-based Verification for Rust Programs (full version)
Authors:
Yusuke Matsushita,
Takeshi Tsukada,
Naoki Kobayashi
Abstract:
Reduction to the satisfiability problem for constrained Horn clauses (CHCs) is a widely studied approach to automated program verification. The current CHC-based methods for pointer-manipulating programs, however, are not very scalable. This paper proposes a novel translation of pointer-manipulating Rust programs into CHCs, which clears away pointers and memories by leveraging ownership. We formal…
▽ More
Reduction to the satisfiability problem for constrained Horn clauses (CHCs) is a widely studied approach to automated program verification. The current CHC-based methods for pointer-manipulating programs, however, are not very scalable. This paper proposes a novel translation of pointer-manipulating Rust programs into CHCs, which clears away pointers and memories by leveraging ownership. We formalize the translation for a simplified core of Rust and prove its correctness. We have implemented a prototype verifier for a subset of Rust and confirmed the effectiveness of our method.
△ Less
Submitted 11 June, 2020; v1 submitted 20 February, 2020;
originally announced February 2020.
-
A Type-Based HFL Model Checking Algorithm
Authors:
Youkichi Hosoi,
Naoki Kobayashi,
Takeshi Tsukada
Abstract:
Higher-order modal fixpoint logic (HFL) is a higher-order extension of the modal mu-calculus, and strictly more expressive than the modal mu-calculus. It has recently been shown that various program verification problems can naturally be reduced to HFL model checking: the problem of whether a given finite state system satisfies a given HFL formula. In this paper, we propose a novel algorithm for H…
▽ More
Higher-order modal fixpoint logic (HFL) is a higher-order extension of the modal mu-calculus, and strictly more expressive than the modal mu-calculus. It has recently been shown that various program verification problems can naturally be reduced to HFL model checking: the problem of whether a given finite state system satisfies a given HFL formula. In this paper, we propose a novel algorithm for HFL model checking: it is the first practical algorithm in that it runs fast for typical inputs, despite the hyper-exponential worst-case complexity of the HFL model checking problem. Our algorithm is based on Kobayashi et al.'s type-based characterization of HFL model checking, and was inspired by a saturation-based algorithm for HORS model checking, another higher-order extension of model checking. We prove the correctness of the algorithm and report on an implementation and experimental results.
△ Less
Submitted 27 August, 2019;
originally announced August 2019.
-
Almost Every Simply Typed Lambda-Term Has a Long Beta-Reduction Sequence
Authors:
Kazuyuki Asada,
Naoki Kobayashi,
Ryoma Sin'ya,
Takeshi Tsukada
Abstract:
It is well known that the length of a beta-reduction sequence of a simply typed lambda-term of order k can be huge; it is as large as k-fold exponential in the size of the lambda-term in the worst case. We consider the following relevant question about quantitative properties, instead of the worst case: how many simply typed lambda-terms have very long reduction sequences? We provide a partial ans…
▽ More
It is well known that the length of a beta-reduction sequence of a simply typed lambda-term of order k can be huge; it is as large as k-fold exponential in the size of the lambda-term in the worst case. We consider the following relevant question about quantitative properties, instead of the worst case: how many simply typed lambda-terms have very long reduction sequences? We provide a partial answer to this question, by showing that asymptotically almost every simply typed lambda-term of order k has a reduction sequence as long as (k-1)-fold exponential in the term size, under the assumption that the arity of functions and the number of variables that may occur in every subterm are bounded above by a constant. To prove it, we have extended the infinite monkey theorem for strings to a parametrized one for regular tree languages, which may be of independent interest. The work has been motivated by quantitative analysis of the complexity of higher-order model checking.
△ Less
Submitted 21 February, 2019; v1 submitted 11 January, 2018;
originally announced January 2018.
-
Higher-Order Program Verification via HFL Model Checking
Authors:
Naoki Kobayashi,
Takeshi Tsukada,
Keiichi Watanabe
Abstract:
There are two kinds of higher-order extensions of model checking: HORS model checking and HFL model checking. Whilst the former has been applied to automated verification of higher-order functional programs, applications of the latter have not been well studied. In the present paper, we show that various verification problems for functional programs, including may/must-reachability, trace properti…
▽ More
There are two kinds of higher-order extensions of model checking: HORS model checking and HFL model checking. Whilst the former has been applied to automated verification of higher-order functional programs, applications of the latter have not been well studied. In the present paper, we show that various verification problems for functional programs, including may/must-reachability, trace properties, and linear-time temporal properties (and their negations), can be naturally reduced to (extended) HFL model checking. The reductions yield a sound and complete logical characterization of those program properties. Compared with the previous approaches based on HORS model checking, our approach provides a more uniform, streamlined method for higher-order program verification.
△ Less
Submitted 27 February, 2018; v1 submitted 24 October, 2017;
originally announced October 2017.
-
Innocent Strategies are Sheaves over Plays---Deterministic, Non-deterministic and Probabilistic Innocence
Authors:
Takeshi Tsukada,
C. -H. Luke Ong
Abstract:
Although the HO/N games are fully abstract for PCF, the traditional notion of innocence (which underpins these games) is not satisfactory for such language features as non-determinism and probabilistic branching, in that there are stateless terms that are not innocent. Based on a category of P-visible plays with a notion of embedding as morphisms, we propose a natural generalisation by viewing inn…
▽ More
Although the HO/N games are fully abstract for PCF, the traditional notion of innocence (which underpins these games) is not satisfactory for such language features as non-determinism and probabilistic branching, in that there are stateless terms that are not innocent. Based on a category of P-visible plays with a notion of embedding as morphisms, we propose a natural generalisation by viewing innocent strategies as sheaves over (a site of) plays, echoing a slogan of Hirschowitz and Pous. Our approach gives rise to fully complete game models in each of the three cases of deterministic, nondeterministic and probabilistic branching. To our knowledge, in the second and third cases, ours are the first such factorisation-free constructions.
△ Less
Submitted 9 September, 2014;
originally announced September 2014.
-
Multi-bifurcations of Wavefronts on r-corners
Authors:
Takaharu Tsukada
Abstract:
We extend the notion of reticular Legendrian unfoldings in order to investigate multi-time bifurcations of wavefronts generated by an r-corner. We give a classification list of generic and stable bifurcations with two time parameter and give all generic figures in the plane and the space.
We extend the notion of reticular Legendrian unfoldings in order to investigate multi-time bifurcations of wavefronts generated by an r-corner. We give a classification list of generic and stable bifurcations with two time parameter and give all generic figures in the plane and the space.
△ Less
Submitted 10 August, 2013;
originally announced August 2013.
-
Genericity of Caustics on a corner
Authors:
Takaharu Tsukada
Abstract:
We introduce the notions of the caustic-equivalence and the weak caustic-equivalence relations of reticular Lagrangian maps in order to give a generic classification of caustics on a corner. We give the figures of all generic caustics on a corner in a smooth manifold of dimension 2 and 3.
We introduce the notions of the caustic-equivalence and the weak caustic-equivalence relations of reticular Lagrangian maps in order to give a generic classification of caustics on a corner. We give the figures of all generic caustics on a corner in a smooth manifold of dimension 2 and 3.
△ Less
Submitted 15 October, 2011; v1 submitted 31 October, 2010;
originally announced November 2010.
-
A Logical Foundation for Environment Classifiers
Authors:
Takeshi Tsukada,
Atsushi Igarashi
Abstract:
Taha and Nielsen have developed a multi-stage calculus λα with a sound type system using the notion of environment classifiers. They are special identifiers, with which code fragments and variable declarations are annotated, and their sco** mechanism is used to ensure statically that certain code fragments are closed and safely runnable. In this paper, we investigate the Curry-Howard isomorphis…
▽ More
Taha and Nielsen have developed a multi-stage calculus λα with a sound type system using the notion of environment classifiers. They are special identifiers, with which code fragments and variable declarations are annotated, and their sco** mechanism is used to ensure statically that certain code fragments are closed and safely runnable. In this paper, we investigate the Curry-Howard isomorphism for environment classifiers by develo** a typed λ-calculus λ|>. It corresponds to multi-modal logic that allows quantification by transition variables---a counterpart of classifiers---which range over (possibly empty) sequences of labeled transitions between possible worlds. This interpretation will reduce the "run" construct---which has a special ty** rule in λα---and embedding of closed code into other code fragments of different stages---which would be only realized by the cross-stage persistence operator in λα---to merely a special case of classifier application. λ|> enjoys not only basic properties including subject reduction, confluence, and strong normalization but also an important property as a multi-stage calculus: time-ordered normalization of full reduction. Then, we develop a big-step evaluation semantics for an ML-like language based on λ|> with its type system and prove that the evaluation of a well-typed λ|> program is properly staged. We also identify a fragment of the language, where erasure evaluation is possible. Finally, we show that the proof system augmented with a classical axiom is sound and complete with respect to a Kripke semantics of the logic.
△ Less
Submitted 27 December, 2010; v1 submitted 19 October, 2010;
originally announced October 2010.
-
Bifurcations of Wavefronts on an r-corner II: Semi-local classification
Authors:
Takaharu Tsukada
Abstract:
We give a classification of generic bifurcations of intersections of wavefronts generated by different points of a hypersurface with or without boundaries.
We give a classification of generic bifurcations of intersections of wavefronts generated by different points of a hypersurface with or without boundaries.
△ Less
Submitted 3 October, 2009;
originally announced October 2009.
-
Bifurcations of Wavefronts on an r-corner
Authors:
Takaharu Tsukada
Abstract:
We introduce the notion of reticular Legendrian unfoldings in order to investigate stabilities of bifurcations of wavefronts generated by a hypersurface germ with a boundary, a corner, or an r-corner in a smooth n dimensional manifold. We define several stabilities of reticular Legendrian unfoldings and prove that they and the stabilities of corresponding generating families are all equivalent and…
▽ More
We introduce the notion of reticular Legendrian unfoldings in order to investigate stabilities of bifurcations of wavefronts generated by a hypersurface germ with a boundary, a corner, or an r-corner in a smooth n dimensional manifold. We define several stabilities of reticular Legendrian unfoldings and prove that they and the stabilities of corresponding generating families are all equivalent and give the classification of generic bifurcations of wavefronts in the cases r=0,n<=5 and r=1,n<= 3respectively.
△ Less
Submitted 23 December, 2010; v1 submitted 29 September, 2009;
originally announced September 2009.
-
Genericity of Caustics and Wavefronts on an r-corner
Authors:
Takaharu Tsukada
Abstract:
We investigate genericities of reticular Lagrangian maps and reticular Legendrian maps in order to give generic classifications of caustics and wavefronts generated by a hypersurface germ without or with a boundary in a smooth manifold.
We investigate genericities of reticular Lagrangian maps and reticular Legendrian maps in order to give generic classifications of caustics and wavefronts generated by a hypersurface germ without or with a boundary in a smooth manifold.
△ Less
Submitted 28 September, 2009;
originally announced September 2009.
