形式言語においては、統語論とモデル理論的意味論の間に明確な対応がある。Montague(1970)(1974)は英語の統語論・意味論も形式言語的理論として与えることができると主張し、形式意味論の分野を切り開いた。Montagueの提示した文法はモンタギュー文法と呼ばれ、内包論理(Intentional Logic)によって、文の意味がその部分の意味、ひいては単語の意味の関数として計算できるという構成性(the principle of compositionality)の概念によって支えられている。しかし形式意味論が発展するにつれ、一般量化子(generalized quantifier)や複数形(plurality)、談話構造(discourse structure)など、内包論理では真理条件を記述できない現象が次々と発見され、80年代の形式意味論はそれらに対して独自の拡張理論を提案してきた。ところが、談話構造におけるEタイプ照応(E-type anaphora)(Evans(1977)(1980),Chierchia(1992))の現象は、Kamp(1981),Kamp & Reyle(1993)の談話表示理論(Discourse Representation Theory)のように、構成的ではない理論に依らなければ真理条件を計算することができないようにみえた。それに対し、Groenendijk & Stokhof(1991)は、単数形のEタイプ照応を扱える構成的な理論として動的述語論理(Dynamic Predicate Logic)を提案したが、Evansが提示した元々のEタイプ照応は、一般量化子を先行詞にもつ複数形の代名詞など、より複雑な場合を含む複合的な問題であった。

　このような背景を受け、本論文では型付き動的論理(Typed Dynamic Logic)という論理言語を新たに提案する。型付き動的論理では、文脈(context)を割り当て関数(assignment function)の集合、そして論理式を文脈間の関数として定義する。この考え方はvan den Berg(1990)の複数形述語論理(Predicate Logic for Plural)と、動的述語論理の関数方式(functional style)の定義を融合させたもので、オーダーを一つ上げるだけで複数形とEタイプ照応の両方を統合的に解決する。型付き動的論理においてはEタイプ解釈が結果として導かれ、談話表示理論やEタイプ論理のような、メカニズムを追加することで解決を図る理論より説明理論として優れている。また、束縛変項照応(bound variable anaphora)や限定表現(definite description)はEタイプ照応の特殊な場合であると主張し、固有名(proper name)や直示代名詞(deictic pronoun)とは別の仕組みであるとする。

　型付き動的論理ではこの考えを更に進め、型付きλ計算に基づいて、すべての論理式を関数として記述することを試みる。通常の論理言語においては、割り当て関数は変数から領域の要素への関数であるが、変数や割り当て関数自体は領域の要素ではないため、λ式で記述することはできない。したがって、文脈から文脈への関数である論理式も、λ式で記述することはできない。これに対し型付き動的論理では論理変数の役割を果たすIndex型と呼ばれる型を導入し、割り当て関数をIndex型からEntity型への関数として定義し、λ演算子によって束縛されるλ式自体の変数に対する割り当て関数(sequence)とは区別する。型付き動的論理の定義を以下列挙する。

(1)　Type

　Type is inductively defined as follows.

(i)　Entity, Index, Truth, Integer, Case∈Type.

(ii) σ,τ∈Type⇒σ/τ,τ＼σ∈Type

(2)　Complex types

　　AF　　　　 ≡def Entity/Index

　　Context　　≡def Truth/AF

　　Prop　　 　≡def Context＼Context

　　 　　　　　≡def (Truth/Entity/.../Entity)＼(Prop/Index/.../Index)

(3)　Truth　Condition　of　Predicates

　　 For any φ:Prop, G:Context,

　　　　φ is consistent in G≡φG=G

　　　　φ is satisfiable in G≡φG≠{}

(4)　Dynamic Predicates and Contexts

　 　For any G:Context,R:Truth/Entity/.../Entity;X,X1,...,Xn:Index,φ,φ:Prop,M,N,n:Integer,

　　　　(R'(X1,...,Xn))(G) = λA.[GA&R(A(X1),...,A(Xn))]

　　　　(φ〓φ)(G)=φ(φ(G))

　　　　(〓φ)(G)=λA.[GA&〜ヨB:A.[(φG)B]]

　　　　(ΔX[φ])(G)= λA.ヨD:Entity.[(φ(λB:AF,[GB&B(X)=D])A)]

　　　　(N=M)(G)=λA.[GA&N=M]

　　　　n!X[φ]=λG.λA,[1φGlX=n&(φG)A]

　　　　nX[φ]=λG.λA.[1φGIX≧n&(φG)A]

　本論文の主題は、このように定義される型付き動的論理が、動的述語論理が完全には成功しなかったEタイプ照応の分析に成功すること、および型付き動的論理の型理論が統語論として機能すること、の二点を示すことである。具体的には、前者の問題として先行詞埋め込み型Eタイプ照応(E-type anaphora with embedded antecedents)、後者の問題として主語位置以外の一般量化子(generalized quantifier in non-subject position)の問題を取り上げる。

　先行詞埋め込み型Eタイプ照応とは、(5)(6)のように、先行詞となる量化子が他の量化子の作用域内に埋め込まれているEタイプ照応である。

(5)　Every boy loves a girl.They/Those girls do not seem all that dissatisfied.

(6)　Every farmer who beats more than half donkeys at his farm makes a profit. But they/those donkeys feel more dead than alive.

　このような照応については、談話表示理論やEタイプ論理(E-type Logic)でも非常に対処しにくい。しかし型付き動的論理では、分散子(distributor)Δをうまく定義することで、これらを埋め込みのない照応と区別せずに正しく分析することができる。また、(5)のように先行詞との数の一致(agreement)がない場合も問題となるが、型付き動的論理では性数の一致を意味論的な演繹条件として記述するため、表層上の不一致は問題とならない。一方、動的述語論理の関数方式の定義では「束縛されていない変数」と「束縛の結果として割り当て先が一つになった変数」を区別できないためこの方法が使えないが、型付き動的論理では存在量化を無作為割り当て(random assignment)によって実現する方式を取らず、論理式を常に文脈からその部分集合を返す関数として定義している。したがって一つのIndexへの割り当て先の数は単調減少となり上述の間題が起こらない。また、文脈が常に割り当て関数に対する特性関数として記述されるため、計算も容易となっている。

　主語位置以外の一般量化子の問題とは、型理論においては自動詞と他動詞の型が異なるため、主語とそれ以外の位置に現れる一般量化子について別々の辞書記述を与えるか、量化子繰り上げ(quantifier raising)のような構成的でない統語操作を仮定するほかはない、という問題である。同様の問題は付加詞(adjunct)についても起こる。これに対し本論文では型付き動的論理の関数適用(functional application)に、線形構造(linear structure)および導出(derivation)という概念を加えた新たな統語論を提案することで解決を図る。

　まず、語の辞書記述は音素または記号の線形構造から、型付き動的論理の式からなる線形構造への導出として定義される。そして動詞からは辞書記述において、名詞と並列的な構造を持っ素動詞(bare verb)と、項の数と同じ数の格付与詞(Case assigner)からなる線形構造が導出される。次に継続(continuation)という概念により、格付与詞の一つが動詞にθ役割を渡すことで動詞は一つ項を取れる型となり、さらに項を取ったのち素動詞と同じ型に戻る。この過程を繰り返すことにより、自動詞と他動詞は導出中で同じ型として現れるのである。これによって、副詞などの付加詞にも複数の辞書記述を与える必要がなくなる。この統語論においては、文法性は「音素または記号の線形構造から、sentence型の型付き動的論理の式が導出できること」として定義され、その式が文の意味表示となる。

　このように本論文は、線形構造の導出に基づく統語論と、型付き動的論理による意味論の組み合わせによって、これまで意味部門から独立した統語部門が存在する証拠とされてきた現象を構成的に解決しつつ、構成的文法を構築するための新たな枠組みを提唱するものである。

　本論文は6章から成っている。第1章では、本研究の背景、目標、概要が述べられている。Montagueは英語の統語論・意味論も形式言語的理論として与えることができる(compositionality)と主張し、形式意味論の分野を切り開いたが、その後の形式意味論の拡張において、compositionalityを達成することは課題となった。このような背景を受け、本論文では意味論として、型付き動的論理という論理言語が新たに提案されている。さらに統語論として、型付き動的論理の型チェックに基づく線形導出の理論が提案されている。

　本論文の第2章と第3章では、型付き動的論理が詳説されている。型付き動的論理では型付きλ計算に基づき、文脈を割り当て関数の集合、論理式を文脈間の関数として定義する。この考え方はvan den Berg(1990)の複数形述語論理と、動的述語論理の関数方式の定義を融合したもので、オーダーを一つ上げるだけで複数形とEタイプ照応の両方を統合的に解決する。

　第3章では、遅延量化という概念が導入される。累積読みとEタイプ読みが、それぞれ量化と照応の基本的な読みであると主張され、分散読みと束縛変項読みは、分散子によって導かれることが示されている。

　本論文の第4章と第5章では、型付き動的論理の型チェックに基づく線形導出の理論が詳説されている。文法性は、音素または記号からなる線形構造から、型付き動的論理の式からなる線形構造への導出という概念、および線形構造中での関数適用によって予測され、同時に意味表示が得られる。また、辞書項目も導出として定義することによって、これまで型理論の問題とされていた「主語位置以外にある一般量化子」について、辞書で量化詞に複数の意味表示を持たせることもなく、また量化子繰り上げのような操作も必要とせずに解決することができる。また、空前置詞による格付与の仕組みも提案されている。

　第6章では、本論文の結論が与えられている。すなわち、型付き動的論理による意味論と、線形導出に基づく統語論の組み合せによって、これまで構成的文法では解決できなかった現象が解決され、新たな構成的文法の枠組みが提唱された。

　以上の結果により、博士(理学)を授与できると認める。