第104回GMSセミナー

日時：2022年7月15日(金)16:30-

場所：岐阜大学工学部11番教室

講師：草刈 圭一朗 氏 (岐阜大学工学部)

題目：関数型プログラムの静的な再帰構造解析に基づく停止性証明手法

概要：プログラミングを学ぶ際の最初の関門の一つが再帰定義であり，多くの方は高校で数列を学ぶ際に漸化式という形で初めて出会うであろう．再帰定義は定義に自分自身を用いるため循環論法に陥る危険性を本質的に孕んでいる．高校で学んだ漸化式では数学的帰納法を土台にしこの危険を回避している．一般に，プログラム中で用いる再帰定義にもなんらかの帰納的な土台が必要となる．逆に，プログラム中の全ての再帰定義になんらかの帰納的な土台を与えることができれば，全ての関数が正しく定義されていることを示すことができ，プログラムの停止性証明を行なうことができる．本講演では，このような観点から設計された静的な再帰構造解析に基づく停止性証明法である静的依存対法を紹介する．また，関数プログラムで広く使用されている高階関数を含む系では直感に反する例が存在し，このような例を静的依存対法がどのように回避しているかも紹介する．