William W. Tait
(サイエンス)
【ういりあむだぶりゅーていと】
アメリカの数学者・哲学者。主に二つの業績がある。
ω論理による無矛盾性証明
種々の数学体系の「有限の立場」からの無矛盾性証明が、ω計算のカットの除去から導かれることを示した。カットの除去の証明には超限帰納法が用いられるが、必要な超限順序数から、体系内で存在が証明できる計算可能関数の増大度などの帰結が得られる。(ordinal analysis)
単純型付きλ計算の強正規性の証明
関数型プログラミング言語のモデルであるλ計算を、静的な型付けが可能なように制限した種々の体系がある。このうちもっとも単純な体系の一つである単純型付λ計算において、項の評価が評価戦略に依らず停止することを示した。この結果はその後種々の型体系に拡張されている。一般に、プログラムの計算結果はプログラムの評価戦略に依存するが、計算結果が評価順序に依らない断片があることを示したことが重要である。(純粋な関数型言語では、停止すれば計算結果が同一であることはチャーチ・ロッサー性の帰結である。)