数理論理学とプログラミング言語から
数理論理学は19世紀末から始まった研究分野です。数学における推論を数学的に研究する分野です。 無限の概念を初めとして様々な人間の直観を超える概念を取り扱うようになったことから、素朴なやり方では論理的なほころびが見つかるようになり、それらに対応するために20世紀初頭から活発に研究がなされました。 コンピュータは同じ頃、開発されました。 数理論理学は数学や計算を研究対象とする分野で、一方で、コンピュータは計算を行う機械であり、プログラムはコンピュータが扱うことができるようにアルゴリズムを記述したものでした。
数理論理学では、「計算ができる」ということをとらえる概念、計算可能性を扱うために概念上のコンピュータが実際のコンピュータの開発と同時期に考案されていました。その後も、数理論理学とコンピュータ／プログラムの関連性については、多様な形で研究が進みました。例えば、プログラムは証明に対応し型が命題に対応するという「カレーハワードの対応」がその一つです。 西崎研究室では、そのような数理論理学とプログラミング言語との関連性を研究の出発点として、プログラミング言語理論やシステム検証等の研究に取り組んでいます。
Mathematical logic is a field of research that began at the end of the 19th century and has been actively studied since the beginning of the 20th century. It is a field that studies reasoning in mathematics mathematically. The relationship between mathematical logic and computer science has been studied in various ways. For example, the similarity between programming languages and deductive systems is one of them. Such similarities are the starting point of our research in the Nishizaki Lab.