Kisoron-ml February 2013

kisoron-ml@fos.kuis.kyoto-u.ac.jp

4 participants
8 discussions

数学基礎論および歴史分科会総会
by KASHIMA Ryo 18 Jun '13

18 Jun '13

日本数学会数学基礎論および歴史分科会会員の皆様、連絡責任評議員の鹿島です。分科会総会の代わりのメールです。ご意見等がありましたらお知らせください。【１】今年の数学基礎論サマースクールはモデル理論がテーマで米田郁生さんが幹事をしてくださります。数学基礎論若手の会の幹事は酒井拓史さんがやってくださると聞きました。例年通り、数学会本部から分科会へ支給される補助金を１万円ずつこの二つの会に出したいと思います。【２】上記の他にも各種研究集会の予定があると思います。分科会ホームページや数学通信に載せていきますので、幹事の方は是非とも情報をお知らせください。５月発行の数学通信に載せるためには、　４月１５日（金）までに鹿島まで情報をお寄せくださるよう、お願いいたします。【３】『数学』編集委員は、現在は池田宏一郎さんですが、４月から鈴木登志雄さんに交代します。【４】現在の分科会運営委員は次のようになっています。（敬称略、括弧内は代表分野、順番は任期の早い順）三宅克哉（歴史）倉田俊彦（計算機科学）高瀬正仁（歴史）山下秀康（超準解析）只木孝太郎（帰納的関数論及び計算理論）桔梗宏孝（モデル理論）安東祐希（証明論）依岡輝幸（集合論）志村立矢（非古典論理）【５】分科会選出評議員は次の通りです：鹿島亮（連絡責任評議員）隈部正博（受賞候補推薦委員）分科会に対するご意見ご質問は評議員またはお近くの運営委員までお寄せください。【６】 3月20日に行われた総会・評議員会での審議決定事項等のうち、重要なものを報告します。 (a) 今後の年会および秋季総合分科会の予定： 9月28(水)〜10月1日(土) 信州大学 2012年３月東京理科大学 2012年９月九州大学 (b) 新理事長に宮岡洋一氏が選出されました。 (c) 早稲田での年会は中止になりましたが、「アブストラクト集が発行されたことによって成立したこととします」だそうです。つまり、今回講演を申し込んだ人はそれを各自の発表業績として数えてよい、ということです。アブストラクト集は数学会本部でとりまとめて今後希望者に販売するそうです。今回講演を申し込んだ人が同じ内容の講演を秋または来春の学会で行うことも可能だそうです。 (c)について、さらに他にも数学会本部からのお知らせは数学会ホームページ： http://mathsoc.jp/ に随時掲載されますので、各自でご確認お願いいたします。【以上】 ----- 鹿島亮東京工業大学大学院情報理工学研究科数理・計算科学専攻 kashima(a)is.titech.ac.jp

1 5

ラムダ計算と論理の早春セミナー3/12--3/16
by Fujita Kenetsu 22 Feb '13

22 Feb '13

『ラムダ計算と論理の早春セミナー』のご案内日程：2013年3月12日(火) 午後5時から3月16日(土) 正午まで場所：国立大学草津セミナーハウス　　　〒377-1711 群馬県吾妻郡草津町大字草津字白根737 詳細：http://komoriyuichi.web.fc2.com/symposium/KusatsuSeminar2008/2013/ 興味をお持ちのみなさまのご参加をお待ちしております． ----------- 群馬大学　藤田憲悦

1 0

Prof. Helmut Schwichtenberg Lecture at NII Logic Seminar
by Makoto Tatsuta 08 Feb '13

08 Feb '13

Prof. Helmut Schwichtenberg Lecture at NII Logic Seminar Date: February 21, 2013, 14:00--16:00 Place: National Institute of Informatics, Lecture Room 1208 (12th floor) 場所: 国立情報学研究所 12階 1208室 (半蔵門線,都営地下鉄三田線・新宿線神保町駅または東西線竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/about/access/) Speaker: Prof. Helmut Schwichtenberg (Ludwig Maximilian University of Munich) Title: Proofs and computations with infinite data Abstract: Ulrich Berger and Monika Seisenberger recently studied extraction from proofs involving (only) abstract reals. They considered a proof using coinduction of the proposition that any two reals in [-1,1] have their average in the same interval, and informally extract a Haskell program working with stream representations of reals. We report on a formalization of this proof, and a machine-extraction of its computational content, in the Minlog proof assistant. This required an extension of this system to also take coinduction into account. The underlying formal system is a theory TCF of computable functionals. It is similar to Heyting arithmetic in all finite types, but with the Scott/Ershov partial continuous functionals as the domain of quantifiers. TCF has free type, predicate and function variables, to allow for abstract developments (groups, fields, real analysis). The underlying inference machinery is minimal logic (implication, universal quantification plus inductively and coinductively defined predicates). Computable functionals (of finite type, with free algebras at ground types) are given by their defining equations. Since the logic is constructive, program extraction by means of a realizability interpretation is possible and a soundness theorem holds. 問合せ先: 龍田真 (国立情報学研究所) e-mail: tatsuta(a)nii.ac.jp http://research.nii.ac.jp/~tatsuta

1 0

Dr. Sam Sanders Lecture at NII Logic Seminar
by Makoto Tatsuta 08 Feb '13

08 Feb '13

Dr. Sam Sanders Lecture at NII Logic Seminar Date: February 13, 2013, 13:30--15:30 Place: National Institute of Informatics, Lecture Room 1904 (19th floor) 場所: 国立情報学研究所 19階 1904室 (半蔵門線,都営地下鉄三田線・新宿線神保町駅または東西線竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/about/access/) Speaker: Dr. Sam Sanders (University of Ghent) Title: Reuniting the antipodes: Bringing together Nonstandard Analysis and Constructive Analysis Abstract: Constructive Analysis (aka BISH) was introduced by Errett Bishop as a redevelopment of Mathematics with a focus on computational content. As such, BISH is based on the BHK (Brouwer-Heyting-Kolmogorov) interpretation of logic, where the notions of `proof' and `algorithm' are central. Constructive Reverse Mathematics (CRM) is a spin-off from Harvey Friedman's `Reverse Mathematics' program where the base theory is based on BISH. In this talk, we introduce an interpretation of BISH in classical Nonstandard Analysis. The role of `proof' in this interpretation is played by the Transfer Principle of Nonstandard Analysis. The role of `algorithm' is played by `$\Omega$-invariance'. Intuitively, an object is $\Omega$-invariant if it does not depend on the *choice* of infinitesimal used in its definition. Using this new interpretation, we obtain many of the well-known results form CRM. In particular, all non-constructive principles (like LPO, LLPO, MP, etc) are interpreted as Transfer Principles, which are not available in our nonstandard base theory. Finally, the interpretation preserves the property that not all $\Delta_1$-formulas are decidable in BISH. We discuss applications in (Homotopy) Type Theory. 問合せ先: 龍田真 (国立情報学研究所) e-mail: tatsuta(a)nii.ac.jp

1 0

Prof. Yue Yang Lecture at NII Logic Seminar
by Makoto Tatsuta 08 Feb '13

08 Feb '13

Prof. Yue Yang Lecture at NII Logic Seminar Date: February 12, 2013, 14:00--16:00 Place: National Institute of Informatics, Lecture Room 1210 (12th floor) 場所: 国立情報学研究所 12階 1210室 (半蔵門線,都営地下鉄三田線・新宿線神保町駅または東西線竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/about/access/) Speaker: Prof. Yue Yang (National University of Singapore) Title: The strength of Ramsey Theorem for Pairs Abstract: Ramsey Theorem is a well-known theorem in combinatorics. However, a special weak form of it (Ramsey Theorem for Pairs) has been a hot topic in Recursion Theory and Reverse Mathematics. In this talk I will give a survey on some recent progresses related to combinatoric principles weaker than Ramsey's Theorem for Pairs. In particular, I will speak about some results obtained by Chitat Chong, Ted Slaman and me on the first order and second order arithmetical consequences of Ramsey Theorem for Pairs. 問合せ先: 龍田真 (国立情報学研究所) e-mail: tatsuta(a)nii.ac.jp http://research.nii.ac.jp/~tatsuta

1 0

仙台ロジックスクール
by Tanaka Kazuyuki 05 Feb '13

05 Feb '13

仙台ロジックスクール SLS2013 （日本ベルギー合同勉強会）すでにご案内申し上げておりますCTFM研究集会(２月１８日〜２１日，東工大) http://sendailogic.math.tohoku.ac.jp/CTFM/ のサテライトとして，仙台にて学生・若手のための勉強会を下記の通り行います。【日程】　２月２２日（金）・２３日（土）9:00 開場【場所】　仙台国際センター　小会議室８【講師】　S. Simpson，Yang Yue，Wu Guohua 　　　　　照井一成，宮部賢志，秋吉亮太（敬称略） ※詳細は，下記ウェブ・ページをご覧ください。 http://sendailogic.math.tohoku.ac.jp/SLS/ 　――――――――――――――――――――――― 参加費は無料ですが，会場準備の都合上，参加される方は事前申し込みをお願いします。【申し込み期限】　2月11日（祝）【申し込み・問い合わせ先】　sendailogic(a)gmail.com 　(担当：朴) 下の申込書をカット＆ペーストして必要事項を記入のうえ，上のアドレス（朴）までお送りください。２２日の夜に懇親会（参加費３千円程度）を予定しておりますので、出欠を併せてお知らせください。 ※　宿泊については，近くのホテルの部屋をいくつかおさえてありますので，必要な方はお問い合わせください。幹事：田中一之，山崎武（東北大学・理学研究科）　――――――――――――――――――――――― 仙台ロジックスクール SLS2013　申込書　お名前　所属・身分　ご連絡先　講演会参加　　22日（　）　23日（　）　懇親会参加　　22日（　）　―――――――――――――――――――――――

1 0

重要なご連絡ーアブストラクトの公開について（訂正）
by Masahiro Kumabe 02 Feb '13

02 Feb '13

皆様複数受け取られた場合はご容赦ください。こんにちは。日本数学会の数学基礎論及び歴史分科会の連絡評議委員の隈部です。先日、学会発表におけるアブストラクトの公開についてのご連絡を、メールにてお知らせしましたが、訂正があります。重要な内容ですので、是非ご一読お願い致します。＊学会における一般講演のアブストラクトについて２０１３年度年会から、数学会として、一般講演のアブストラクトをPDFファイルとして、学会開催前に、数学会のホームペジにて公開することをご連絡しましたが、これは、数学基礎論及び歴史分科会においては、学会会員内だけの公開です。昨年９月の分科会総会でそのように決まっていました。ここにお詫びして訂正致します。申し訳ありませんでした。従いまして、学会会員でない方は、アブストラクトの冊子を学会会場で購入してご覧になれます。以上の件、お間違いのないようにご理解ください。隈部

1 0

Eighth NII Type Theory Workshop
by Makoto Tatsuta 01 Feb '13

01 Feb '13

Eighth NII Type Theory Workshop Date: February 6, 2013, 10:40--16:50 Place: National Institute of Informatics, Room 1904 (19th floor) 場所: 国立情報学研究所 19階 1904室 (半蔵門線,都営地下鉄三田線・新宿線神保町駅または東西線竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/about/access/) Program: 10:40--11:20 Toshihiko Uchida (The Graduate University for Advanced Studies) Title: A Partial Translation from lambda U to lambda 2 11:20--12:00 Daisuke Kimura (National Institute of Informatics) Title: Linear Pure Type Systems 12:00--14:00 Lunch Break 14:00--14:40 Kazuyuki ASADA (National Institute of Informatics) Title: Curry-Howard Correspondence between Dialectica Interpretation and Bidirectional Transformation 14:40--15:20 Makoto Tatsuta (National Institute of Informatics) Title: Dual Calculus with Inductive and Coinductive Types 15:20--15:50 Tea Break 15:50--16:50 Stefano Berardi (Torino University) Title: A Curry-Howard result for various subclassical logics Abstracts: ---------------------------------------------------------------------- Toshihiko Uchida (The Graduate University for Advanced Studies) Title: A Partial Translation from lambda U to lambda 2 Abstract: Girard showed that every type of sort * (i.e., proposition) is inhabited in lambda U. Barendregt state without proof that every type of sort Box (i.e., domain) is also inhabited in the system. In this talk, we show that the second statement is not the case by giving a partial translation from lambda U to lambda 2. ---------------------------------------------------------------------- Daisuke Kimura (National Institute of Informatics) Title: Linear Pure Type Systems Abstract: This talk proposes a linear variant of Pure Type Systems (PTSs), called linear pure type systems (LPTSs). It is a general framework, which provides a uniform way to treat various linear type systems that have the features of linear logic. We first introduce a subframework of LPTSs, called multiplicative linear pure type systems (MLPTSs), in which only variables that linearly occur are abstracted. All MLPTSs are consistent and satisfy strong normalization. However their expressive power is rather weak. We then give LPTSs by extending MLPTSs with exponentials. Each PTS can be embedded into a LPTS. We also show the equivalence of strong normalizability of PTSs and LPTSs by giving mutual translations between them. ---------------------------------------------------------------------- Kazuyuki ASADA (National Institute of Informatics) Title: Curry-Howard Correspondence between Dialectica Interpretation and Bidirectional Transformation Abstract: We give Curry-Howard style correspondence between (propositional logic part of) Dialectica interpretation and bidirectional transformation. Dialectica interpretation was introduced by Godel to show relative consistency of Heyting Arithmetic to System T. Independently, bidirectional transformation arose in database community for automatic view-update problem, and recently have been studied in programming language community to formulate languages for bidirectional transformations. A bidirectional transformation consists of a pair of forward ("usual") transformation and a backward ("inverse") transformation, and we usually assume that they satisfy some standard axioms called GetPut law and PutGet law. We show GetPut law naturally fits the above correspondence to Dialectica interpretation, and this gives a way of extending a language for bidirectional transformations with GetPut law. Then we modify the above scheme for PutGet law and the combination of GetPut and PutGet laws. We also show that Paiva's variant of Dialectica model, GC, corresponds to the category for inverse computation. Then for the result by Paiva that the original Dialectica category is the coKleisli category of some comonad on GC, we give similar result for PutGet law, and we utilize this to investigate further categorical structures of these models. Also we see that a kind of Diller-Nahm variant of Dialectica interpretation corresponds to backward-partial bidirectional transformation. ---------------------------------------------------------------------- Makoto Tatsuta (National Institute of Informatics) Title: Dual Calculus with Inductive and Coinductive Types Abstract: This talk gives an extension of Dual Calculus by introducing inductive types and coinductive types. The same duality as Dual Calculus is shown to hold in the new system, that is, this talk presents its involution for the new system and proves that it preserves both typing and reduction. The duality between inductive types and coinductive types is shown by the existence of the involution that maps an inductive type and a coinductive type to each other. The strong normalization in this system is also proved. First, strong normalization in second-order Dual Calculus is shown by translating it into second-order symmetric lambda calculus. Next, strong normalization in Dual Calculus with inductive and coinductive types is proved by translating it into second-order Dual Calculus. This is a joint work with Daisuke Kimura. ---------------------------------------------------------------------- Stefano Berardi (Torino University) Title: A Curry-Howard result for various subclassical logics Abstract: We introduce games with Sequential Backtracking as a model for various sub-classical logic that have implication as a primitive connective. We define a one-sided version of the logical systems, whose proofs have a tree isomorphism (a kind of ``Curry Howard'' isomorphism) with respect to the winning strategies of the game semantics. We use this correspondence to interpret various classical proofs as learning algorithms. ---------------------------------------------------------------------- 問合せ先　龍田 (tatsuta(a)nii.ac.jp)

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Kisoron-ml February 2013