論文の公開元へ

書き出し

Refer/BibIX

RIS

BibTeX

TSV

Formalization of Equational Reasoning in the Set-Theoretic Interpretation of Type Theory

Saikawa, Takafumi 才川, 隆文名古屋大学

2020.05.14

概要

学位報告４

別紙４
報告番号

※

第

号

主論文の要旨
論文題目 Formalization of Equational Reasoning in the SetTheoretic Interpretation of Type Theory
(型理論の集合論的意味論を用いた等式変形証明法の形式化)
氏名
才川隆文

論文内容の要旨
The method of equational reasoning is a style for mathematical proofs
which heavily uses rewriting along equations.
Not only values but propositions are rewritten using equivalence lemmas.
This style is common in proofs of pure mathematics but not so much in proofs
written using computerized proof assistants. Proofs assistants are softwares
that aid human users to write and check mathematical proofs. They are based
on systems of formal logic, in which proofs are expressed as tree structures.
Using such representations of proofs, it is easier for the users of proof
assistants to proceed with a deductive style of proof.
These two styles are quite different in terms of the management of hypotheses
in the proofs. The deductive style of proofs traverses and constructs a tree of
proofs. The hypotheses may appear or disappear based on the shape of tree,
resulting in the localization of proofs at each point of the proof tree.
On the other hand, equational rewriting basically does not discard hypotheses.
One can chain many steps of reasoning without paying constant attention to
the proof tree structure: they are freed from the low-level tree expression of

学位関係

proofs.
This thesis is based upon the foundational studies on formal logic,
especially on equational reasoning. We formalize using a proof assistant
various aspects of equational reasoning. Especially we focus on the
formalization of monadic equational reasoning on effects. Effects are
features of computer programs that have been long considered to be a difficult
target for equational reasoning. We have worked out a framework to formally
perform equational reasoning on the effects of programs.
The formalization includes both theories which are applied to proofs on
concrete programs, and models which assure the consistency of those theories.
We also extend the method of equational reasoning by developing a framework
for category theory. This framework features the use of concrete categories
on the contrary to many other formalization attempts. This design choice
leads to the lightweight usability of our framework. It enables shallow
embedding and direct reasoning on programs whose properties can only be
captured at categorical level. As a specific example, we construct the first
formalized model of the theory of combined probabilistic and nondeterministic
choice. It has been the subject of extensive research and is known to be tricky.
This construction of model is backed by the formalization of convex spaces.
Convex spaces arise as an algebraic abstraction of convex sets in vector spaces.
They appear in various domains of pure and applied mathematics.
Although it is also an equational theory, it is poor in algebraic properties
such as linearity of vector operations and does not allow easy rewriting.
We investigated its accompanying theory of conical spaces, which is an
abstraction of real cones in vector spaces, and have proper linearity in its
operations. We have devised a method to prove properties of convex spaces by
embedding them into conical spaces and projecting them back. This method
was only recently noticed in the literature and our specific applications turns
out to be new.

論文の公開元へ

参考文献

[Aczel, 1977] Aczel, P. (1977). An introduction to inductive definitions**most of this paper was

prepared while the author was visiting caltech. supported hy nsf grant 75-07562. In Barwise, J.,

editor, Handbook of Mathematical Logic, volume 90 of Studies in Logic and the Foundations of

Mathematics, pages 739 – 782. Elsevier. (Cited on pages 27 and 28.)

[Affeldt et al., 2020a] Affeldt, R., Garrigue, J., Nowak, D., and Saikawa, T. (2020a). Monadic

equational reasoning in Coq. https://github.com/affeldt-aist/monae/. Coq scripts. (Cited

on pages 4, 51, 52, 53, 54, 55, 56, 61, 65, 66, 67, 69, and 70.)

[Affeldt et al., 2016] Affeldt, R., Garrigue, J., and Saikawa, T. (2016). Formalization of ReedSolomon codes and progress report on formalization of LDPC codes. In International Symposium

on Information Theory and Its Applications (ISITA 2016), Monterey, California, USA, October

30–November 2, 2016, pages 537–541. IEICE. IEEE Xplore. (Cited on page 1.)

[Affeldt et al., 2018] Affeldt, R., Garrigue, J., and Saikawa, T. (2018). Examples of formal proofs

about data compression. In International Symposium on Information Theory and Its Applications

(ISITA 2018), Singapore, October 28–31, 2018, pages 665–669. IEICE. IEEE Xplore. (Cited on

pages 1 and 41.)

[Affeldt et al., 2020b] Affeldt, R., Garrigue, J., and Saikawa, T. (2020b). A library for formalization

of linear error-correcting codes. Journal of Automated Reasoning. (Cited on page 1.)

[Affeldt et al., 2020c] Affeldt, R., Garrigue, J., and Saikawa, T. (2020c). Reasoning with conditional probabilities and joint distributions in Coq. Computer Software. Accepted by Computer

Software, ISSN: 0289-6540. (Cited on page 1.)

[Affeldt et al., 2014] Affeldt, R., Hagiwara, M., and S´enizergues, J. (2014). Formalization of Shannon’s theorems. Journal of Automated Reasoning, 53(1):63–103. (Cited on page 35.)

[Affeldt et al., 2019] Affeldt, R., Nowak, D., and Saikawa, T. (2019). A hierarchy of monadic

effects for program verification using equational reasoning. In Hutton, G., editor, Mathematics

of Program Construction, pages 226–254, Cham. Springer International Publishing. (Cited on

pages 1, 48, and 56.)

[Ahrens et al., 2019a] Ahrens, B., Frumin, D., Maggesi, M., and van der Weide, N. (2019a). Bicategories in Univalent Foundations. In Geuvers, H., editor, 4th International Conference on

Formal Structures for Computation and Deduction (FSCD 2019), volume 131 of Leibniz International Proceedings in Informatics (LIPIcs), pages 5:1–5:17, Dagstuhl, Germany. Schloss

Dagstuhl–Leibniz-Zentrum fuer Informatik. (Cited on page 72.)

[Ahrens et al., 2018] Ahrens, B., Hirschowitz, A., Lafont, A., and Maggesi, M. (2018). High-Level

Signatures and Initial Semantics. In Ghica, D. and Jung, A., editors, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018), volume 119 of Leibniz International Proceedings

in Informatics (LIPIcs), pages 4:1–4:22, Dagstuhl, Germany. Schloss Dagstuhl–Leibniz-Zentrum

fuer Informatik. (Cited on page 72.)

[Ahrens et al., 2019b] Ahrens, B., Hirschowitz, A., Lafont, A., and Maggesi, M. (2019b). Modular

Specification of Monads Through Higher-Order Presentations. In Geuvers, H., editor, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), volume

131 of Leibniz International Proceedings in Informatics (LIPIcs), pages 6:1–6:19, Dagstuhl, Germany. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik. (Cited on page 72.)

[Barendregt, 1991] Barendregt, H. (1991). Introduction to generalized type systems. Journal of

Functional Programming, 1(2):125–154. (Cited on page 25.)

[Barr and Wells, 1985] Barr, M. and Wells, C. (1985). Toposes, Triples and Theories. SpringerVerlag, New York. (Cited on page 47.)

[Barras, 2010] Barras, B. (2010). Sets in coq, coq in sets. Journal of Formalized Reasoning,

3(1):29–48. (Cited on page 27.)

[Beaulieu, 2008] Beaulieu, G. (2008). Probabilistic completion of nondeterministic models. PhD

thesis, University of Ottawa. (Cited on pages 68 and 69.)

[Bertot et al., 2008] Bertot, Y., Gonthier, G., Ould Biha, S., and Pasca, I. (2008). Canonical big

operators. In Mohamed, O. A., Mu˜

noz, C., and Tahar, S., editors, Theorem Proving in Higher

Order Logics, pages 86–101, Berlin, Heidelberg. Springer Berlin Heidelberg. (Cited on page 39.)

[Bird, 1987] Bird, R. S. (1987). An introduction to the theory of lists. In Broy, M., editor, Logic

of Programming and Calculi of Discrete Design, pages 5–42, Berlin, Heidelberg. Springer Berlin

Heidelberg. (Cited on page 9.)

[Bird, 1989] Bird, R. S. (1989). Algebraic Identities for Program Calculation. The Computer

Journal, 32(2):122–126. (Cited on page 9.)

[Bonchi et al., 2017] Bonchi, F., Silva, A., and Sokolova, A. (2017). The Power of Convex Algebras.

In Meyer, R. and Nestmann, U., editors, 28th International Conference on Concurrency Theory

(CONCUR 2017), volume 85 of Leibniz International Proceedings in Informatics (LIPIcs), pages

23:1–23:18, Dagstuhl, Germany. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik. (Cited on

pages 35, 36, and 71.)

[Cheung, 2017] Cheung, K.-H. (2017). Distributive Interaction of Algebraic Effects. PhD thesis,

University of Oxford. (Cited on pages 63, 67, 68, and 71.)

[Church, 1932] Church, A. (1932). A set of postulates for the foundation of logic. Annals of

Mathematics, 33(2):346–366. (Cited on page 25.)

[Church, 1936] Church, A. (1936). An unsolvable problem of elementary number theory. American

Journal of Mathematics, 58(2):345–363. (Cited on page 25.)

[Coquand and Huet, 1988] Coquand, T. and Huet, G. (1988). The calculus of constructions. Information and Computation, 76(2):95 – 120. (Cited on page 25.)

[Cover and Thomas, 2006] Cover, T. M. and Thomas, J. A. (2006). Elements of information theory.

Wiley. 2nd ed. (Cited on pages 33 and 44.)

[Crhak, 2018a] Crhak, T. (2018a). A note on σ-algebras on sets of affine and measurable maps to

the unit interval. (Cited on page 72.)

[Crhak, 2018b] Crhak, T. (2018b). On functors from category of giry algebras to category of convex

spaces. (Cited on page 72.)

[Dockins, 2014] Dockins, R. (2014). Formalized, effective domain theory in coq. In Klein, G. and

Gamboa, R., editors, Interactive Theorem Proving, pages 209–225, Cham. Springer International

Publishing. (Cited on page 72.)

[eter J. Freyd, 1970] eter J. Freyd (1970). Homotopy is not concrete. In Peterson, F. P., editor,

The Steenrod Algebra and Its Applications: A Conference to Celebrate N.E. Steenrod’s Sixtieth

Birthday, pages 25–34, Berlin, Heidelberg. Springer Berlin Heidelberg. (Cited on page 72.)

[Flood, 1981] Flood, J. (1981). Semiconvex geometry. Journal of the Australian Mathematical

Society, 30(4):496–510. (Cited on pages 33, 37, 38, and 46.)

[Freyd, 1973] Freyd, P. J. (1973). Concreteness. Journal of Pure and Applied Algebra, 3(2):171 –

191. (Cited on page 65.)

[Fritz, 2009] Fritz, T. (2009). Convex spaces i: Definition and examples. (Cited on page 34.)

[Garillot et al., 2009] Garillot, F., Gonthier, G., Mahboubi, A., and Rideau, L. (2009). Packaging

mathematical structures. In TPHOLs, volume 5674 of Lecture Notes in Computer Science, pages

327–342. Springer. (Cited on pages 29 and 34.)

[Gibbons, 2012] Gibbons, J. (2012). Unifying theories of programming with monads. In Wolff,

B., Gaudel, M., and Feliachi, A., editors, Unifying Theories of Programming, 4th International

Symposium, UTP 2012, Paris, France, August 27-28, 2012, Revised Selected Papers, volume

7681 of Lecture Notes in Computer Science, pages 23–67. Springer. (Cited on page 55.)

[Gibbons and Hinze, 2011] Gibbons, J. and Hinze, R. (2011). Just do it: simple monadic equational

reasoning. In 16th ACM SIGPLAN Int. Conf. on Functional Programming (ICFP 2011), Tokyo,

Japan, September 19–21, 2011, pages 2–14. ACM. (Cited on pages 4, 10, 48, 50, 59, and 68.)

[Girard, 1972] Girard, J.-Y. (1972). Interpr´etation fonctionnelle et ´elimination des coupures de

l’arithm´etique d’ordre sup´erieur. PhD thesis, Universit´e Paris Diderot. (Cited on page 25.)

[Girard et al., 1989] Girard, J.-Y., Taylor, P., and Lafont, Y. (1989). Proofs and Types. Cambridge

University Press, USA. (Cited on page 27.)

[Goncharov and Schr¨

oder, 2011] Goncharov, S. and Schr¨oder, L. (2011). A counterexample to

tensorability of effects. In Corradini, A., Klin, B., and Cˆırstea, C., editors, Algebra and Coalgebra

in Computer Science, pages 208–221, Berlin, Heidelberg. Springer Berlin Heidelberg. (Cited on

pages 71 and 72.)

[Infotheo, 2020] Infotheo (2020). A Coq formalization of information theory and linear errorcorrecting codes. https://github.com/affeldt-aist/infotheo/. Coq scripts. (Cited on

pages 34, 36, 38, 39, 40, 41, 42, 43, 44, 45, 66, 68, and 69.)

[Jacobs, 2010] Jacobs, B. (2010). Convexity, duality and effects. In IFIP TCS, volume 323 of

IFIP Advances in Information and Communication Technology, pages 1–19. Springer. (Cited on

pages 34, 36, and 72.)

[Jones and Plotkin, 1989] Jones, C. and Plotkin, G. D. (1989). A probabilistic powerdomain of

evaluations. In [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science,

pages 186–195. (Cited on pages 46 and 71.)

[Keimel and Plotkin, 2016] Keimel, K. and Plotkin, G. (2016). Mixed powerdomains for probability

and nondeterminism. Logical Methods in Computer Science, 13. (Cited on pages 33, 40, 46,

and 72.)

[Keimel and Plotkin, 2009] Keimel, K. and Plotkin, G. D. (2009). Predicate transformers for

extended probability and non-determinism. Mathematical Structures in Computer Science,

19(3):501–539. (Cited on page 46.)

[Kirch, 1993] Kirch, O. (1993). Bereiche und bewertungen. Master’s thesis, Technischen Hochschule

Darmstadt. (Cited on pages 33 and 46.)

[Kunen, 2009] Kunen, K. (2009). The Foundations of Mathematics, volume 19 of Studies in Logic,

Mathematical Logic and Foundations. College Publications. (Cited on page 17.)

[Lee and Werner, 2011] Lee, G. and Werner, B. (2011). Proof-irrelevant model of cc with predicative induction and judgmental equality. Logical Methods in Computer Science, 7(4). (Cited on

page 27.)

[Linton, 1966] Linton, F. E. J. (1966). Some aspects of equational categories. In Eilenberg, S., Harrison, D. K., MacLane, S., and R¨

ohrl, H., editors, Proceedings of the Conference on Categorical

Algebra, pages 84–94, Berlin, Heidelberg. Springer Berlin Heidelberg. (Cited on page 47.)

[Mac Lane, 1998] Mac Lane, S. (1998). Categories for the Working Mathematician, volume 5 of

Graduate Texts in Mathematics. Springer-Verlag, Berlin and New York, second edition. (Cited

on page 48.)

[Mahboubi and Tassi, 2013] Mahboubi, A. and Tassi, E. (2013). Canonical structures for the working Coq user. In 4th Int. Conf. on Interactive Theorem Proving (ITP 2013), Rennes, France,

July 22–26, 2013, volume 7998 of Lecture Notes in Computer Science, pages 19–34. Springer.

(Cited on page 29.)

[Martin-L¨of, 1984] Martin-L¨

of, P. (1984). Intuitionistic type theory. Bibliopolis. (Cited on page 27.)

[McBride, 1999] McBride, C. (1999). Dependently Typed Functional Programs and their Proofs.

PhD thesis, University of Edinburgh. (Cited on page 72.)

[Meng, 1987] Meng, X.-Q. (1987). Categories of Convex Sets and of Metric Spaces with Applications

to Stochastic Programming and Related Areas. PhD thesis, State University of New York at

Buffalo. (Cited on page 72.)

[Miquel and Werner, 2003] Miquel, A. and Werner, B. (2003). The not so simple proof-irrelevant

model of cc. In Geuvers, H. and Wiedijk, F., editors, Types for Proofs and Programs, pages

240–258, Berlin, Heidelberg. Springer Berlin Heidelberg. (Cited on page 27.)

[Mislove, 2000] Mislove, M. (2000). Nondeterminism and probabilistic choice: Obeying the laws.

In Palamidessi, C., editor, CONCUR 2000 — Concurrency Theory, pages 350–365, Berlin, Heidelberg. Springer Berlin Heidelberg. (Cited on page 71.)

[Mislove et al., 2004] Mislove, M., Ouaknine, J., and Worrell, J. (2004). Axioms for probability

and nondeterminism. Electronic Notes in Theoretical Computer Science, 96:7 – 28. Proceedings

of the 10th International Workshop on Expressiveness in Concurrency. (Cited on page 55.)

[Moggi, 1989] Moggi, E. (1989). Computational lambda-calculus and monads. In LICS, pages

14–23. IEEE Computer Society. (Cited on pages 10 and 47.)

[Morgan et al., 1996] Morgan, C., Mciver, A., Seidel, K., and Sanders, J. W. (1996). Refinementoriented probability for csp. Form. Asp. Comput., 8(6):617–647. (Cited on page 55.)

[Mu, 2019] Mu, S.-C. (2019). Equational reasoning for non-deterministic monad: A case study of

Spark aggregation. Technical Report TR-IIS-19-002, Institute of Information Science, Academia

Sinica. (Cited on pages 4 and 56.)

[Neumann, 1970] Neumann, W. D. (1970). On the quasivariety of convex subsets of affine spaces.

Archiv der Mathematik, 21:11–16. (Cited on page 46.)

[Paulin-Mohring, 2015] Paulin-Mohring, C. (2015). Introduction to the Calculus of Inductive Constructions. In Paleo, B. W. and Delahaye, D., editors, All about Proofs, Proofs for All, volume 55 of Studies in Logic (Mathematical logic and foundations). College Publications. (Cited

on page 25.)

[Plotkin and Power, 2001] Plotkin, G. and Power, J. (2001). Semantics for algebraic operations.

Electronic Notes in Theoretical Computer Science, 45:332 – 345. MFPS 2001,Seventeenth Conference on the Mathematical Foundations of Programming Semantics. (Cited on pages 10 and 48.)

[Plotkin, 1976] Plotkin, G. D. (1976). A powerdomain construction. SIAM J. Comput., 5:452–487.

(Cited on page 71.)

[Plotkin, 1983] Plotkin, G. D. (1983). Pisa notes on domain theory. (Cited on page 71.)

[Plotkin and Power, 2002] Plotkin, G. D. and Power, J. (2002). Notions of computation determine monads. In FoSSaCS, volume 2303 of Lecture Notes in Computer Science, pages 342–356.

Springer. (Cited on page 48.)

[Reiterman, 1986] Reiterman, J. (1986). On locally small based algebraic theories. Commentationes

Mathematicae Universitatis Carolinae, 27(2):325–340. (Cited on page 68.)

[Reynolds, 1984] Reynolds, J. C. (1984). Polymorphism is not set-theoretic. In Kahn, G., MacQueen, D. B., and Plotkin, G., editors, Semantics of Data Types, pages 145–156, Berlin, Heidelberg. Springer Berlin Heidelberg. (Cited on page 27.)

[Semadini, 1971] Semadini, Z. (1971). Banach Spaces of Continuous Functions. PWN. (Cited on

page 46.)

[Shoenfield, 1967] Shoenfield, J. R. (1967).

page 17.)

Mathematical Logic.

Addison-Wesley.

(Cited on

[Stone, 1949] Stone, M. H. (1949). Postulates for the barycentric calculus. Ann. Mat. Pura Appl.,

29(1):25–30. (Cited on pages 33, 34, 36, 37, and 39.)

[Swirszcz,

1974] Swirszcz,

T. (1974). Monadic functors and convexity. Bulletin de l’Acad´emie

polonaise des sciences. S´erie des sciences math´ematiques, astronomiques et physiques, 22(1).

(Cited on pages 34 and 72.)

[Tix et al., 2009] Tix, R., Keimel, K., and Plotkin, G. (2009). Semantic domains for combining

probability and non-determinism. Electronic Notes in Theoretical Computer Science, 222:3 – 99.

(Cited on pages 46 and 72.)

[van Heerdt et al., 2018] van Heerdt, G., Hsu, J., Ouaknine, J., and Silva, A. (2018). Convex

language semantics for nondeterministic probabilistic automata. In Fischer, B. and Uustalu,

T., editors, Theoretical Aspects of Computing – ICTAC 2018, pages 472–492, Cham. Springer

International Publishing. (Cited on pages 34, 35, and 71.)

[Varacca and Winskel, 2006] Varacca, D. and Winskel, G. (2006). Distributing probability over

non-determinism. Mathematical Structures in Computer Science, 16(1):87–113. (Cited on

pages 33, 37, 46, 63, 69, and 71.)

[Wadler, 1990] Wadler, P. (1990). Comprehending monads. In LISP and Functional Programming,

pages 61–78. (Cited on pages 10 and 48.)

[Werner, 1997] Werner, B. (1997). Sets in types, types in sets. In Abadi, M. and Ito, T., editors,

Theoretical Aspects of Computer Software, pages 530–546, Berlin, Heidelberg. Springer Berlin

Heidelberg. (Cited on page 27.)

[Williams, 1969] Williams, N. H. (1969). On grothendieck universes. Compositio Mathematica,

21(1):1–3. (Cited on page 28.)

[Winskel, 1983] Winskel, G. (1983). A note on powerdomains and modality. In Karpinski, M.,

editor, Foundations of Computation Theory, pages 505–514, Berlin, Heidelberg. Springer Berlin

Heidelberg. (Cited on page 72.)

[Yi and Larsen, 1992] Yi, W. and Larsen, K. G. (1992). Testing probabilistic and nondeterministic

processes. In LINN, R. and UYAR, M., editors, Protocol Specification, Testing and Verification,

XII, IFIP Transactions C: Communication Systems, pages 47 – 61. Elsevier, Amsterdam. (Cited

on page 55.)

...

参考文献をもっと見る

分野

大学

学位論文種類・取得年

言語

Formalization of Equational Reasoning in the Set-Theoretic Interpretation of Type Theory

概要

関連論文

クライン群の可視化手法とその芸術表現への広がりに関する研究

進化ゲーム理論、実験･シミュレーション及び応用面から見る協調創発

AN ESTIMATE FOR SURFACE MEASURE OF SMALL BALLS IN CARNOT GROUPS

Pointwise convergence problems and some sharp inequalities arising in quantum mechanics

On branching laws of Speh representations

参考文献

分野

大学

学位論文種類・取得年

言語

コピーが完了しました

URLをコピーしました

Formalization of Equational Reasoning in the Set-Theoretic Interpretation of Type Theory

概要

関連論文

クライン群の可視化手法とその芸術表現への広がりに関する研究

進化ゲーム理論、実験･シミュレーション及び応用面から見る協調創発

AN ESTIMATE FOR SURFACE MEASURE OF SMALL BALLS IN CARNOT GROUPS

Pointwise convergence problems and some sharp inequalities arising in quantum mechanics

On branching laws of Speh representations

参考文献