• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

型理論とその周辺

Research Project

Project/Area Number 08640256
Research Category

Grant-in-Aid for Scientific Research (C)

Allocation TypeSingle-year Grants
Section一般
Research Field General mathematics (including Probability theory/Statistical mathematics)
Research InstitutionTokyo Institute of Technology

Principal Investigator

寶来 正子  東京工業大学, 大学院・情報理工学研究科, 教授 (00015588)

Co-Investigator(Kenkyū-buntansha) 大槻 知忠  東京工業大学, 大学院・情報理工学研究科, 助教授 (50223871)
高橋 渉  東京工業大学, 大学院・情報理工学研究科, 助教授 (40016142)
小島 定吉  東京工業大学, 大学院・情報理工学研究科, 教授 (90117705)
鵜飼 正二  東京工業大学, 大学院・情報理工学研究科, 教授 (30047170)
藤井 光昭  大学入試センター, 教授 (70016343)
Project Period (FY) 1996
Project Status Completed (Fiscal Year 1996)
Budget Amount *help
¥2,400,000 (Direct Cost: ¥2,400,000)
Fiscal Year 1996: ¥2,400,000 (Direct Cost: ¥2,400,000)
Keywords型理論 / ラムダ計算
Research Abstract

型理論の研究で明らかにしたい事柄の一つに,与えられた型システムで型付け可能な項全体を適当な同値関係(例えば,β同値,βη同値,またはその他の同値関係)の下で同値類に分類したとき,その全体がどのような数学的構造を成すかを知ることが上げられる.これは本来,意味論の中心的な研究課題であると言えるが,型理論の場合,この問題に対して構文論(または証明論)的なアプローチの可能性が考えられる.
本研究では,構文論的アプローチによって,単純型理論における型付き項全体を,同値関係βηで割った商集合を,ある種の文法的手法を用いて表現することに成功した.ここで用いた手法は,文脈自由文法の名で親しまれている概念を,この目的のために拡張したもので,述語論理における項や,これを拡張した種々の型理論の項から成る集合を端的に表現できる一般的な枠組みであり,今後,単純型以外の種々の体系に対しても,有用性を発揮することが期待される.
この,新たに導入した文法的方法の一つの応用として,型理論の型付き項を用いて,自由代数構造の上のどのような関数が表現可能かを調べる問題が上げられる.型のないラムダ計算の項を用いて表現可能な自然数関数はちょうど計算可能関数と一致し,単純型理論の場合はそれが拡張多項式と一致することが知られているが,これを一般の自由代数構造上の関数に拡張すると,単純型理論の場合でも議論が非常に複雑になり,その結果,表現可能な関数についてある種の特徴付けがすでに得られているものの,満足のいく結果とは言い難い.この問題に対して,我々の文法的手法を用いて,既存の結果とは異なる見通しの良い新しい特徴付けを得ることができた.この結果を更に単純型以外の型理論に拡張する試みを今後続けたいと計画している.

Report

(1 results)
  • 1996 Annual Research Report
  • Research Products

    (6 results)

All Other

All Publications (6 results)

  • [Publications] M.Takahashi,Y.Akama and S.Hirokawa: "Normal proofs and their grammar" Information & Computation. 125. 144-153 (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] M.Huzii and C.Chen: "Statistical Properties of a Predictor for a Seasonal Time Series When its Residual Deviates from a Stationary Process" Probability Theory and Mathematical Statistics,Proceedings of Seventh Japan-Russian Symposium. 132-146 (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] H.Morimoto and S.Ukai: "Perturbation of the Navier-Stokes flow in an annular domain with the non-vanishing outflow condition" J.Math.Sci.Univ.Tokyo. 3. 73-82 (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] S.Kojima: "Nonsingular parts of hyperbolic 3-cone-manifolds" Topology and Teichmuller spaces,World Scientific Pub.115-122 (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] S.Kojima: "Immersed geodesic surfaces in heperbolic 3-manifolds" Complex variables. 29. 45-58 (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] A.T.Lau and W.Takahashi: "Invariant submeans and semigroups of nonexpansive mappings on Banach spaces with normal structure" Journal of Functional Analysis. 142-1. 79-88 (1996)

    • Related Report
      1996 Annual Research Report

URL: 

Published: 1996-04-01   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi