ホットの本では、タイプ形成者の大半は冗長ですか?もしそうなら、なぜですか?

Hott book
の第1章および付録Aでは、いくつかの基本型ファミリが紹介されています(ユニバースタイプ、依存する関数タイプ、Coproduct型、空型、単位型、自然数型、およびID型)を使用して、ホモトピー型理論の基礎を形成します。

しかし、宇宙型と従属関数型があれば、これらの他のすべての「プリミティブ」型を構築することができます。たとえば、Empty型は代わりに次のように定義できます。

ΠT:U.T

私は他のタイプも、純粋なCC
の中にあるように構築できると考えています。(つまり、定義の帰納的部分から型​​を導出するだけです)。

これらのタイプの多くは、第5章と第6章で紹介したInductive/Wタイプによって明示的に冗長化されています。しかし、Inductive/WタイプはHoTTとの相互作用に関するオープンな質問があるため、少なくとも本が出てきたとき)。

ですから、これらの追加タイプがなぜプリミティブとして提示されるのか、私は非常に混乱しています。私の直感は、基礎理論が可能な限り最小限でなければならず、冗長Empty型を原則として理論に再定義することは非常に恣意的であるように思われる。

この選択はなされましたか

  • 私が気づいていないいくつかのメタセオライティックな理由のために?
  • 歴史的な理由から、型理論のように見えるようにする 過去のタイプ理論(必ずしもそうしようとはしていなかった 基礎)?
  • コンピュータインタフェースの「使いやすさ」を考えている?
  • 私が気づいていない校正検索でいくつかの利点がありますか?

Similar to:
Minimal specification of Martin-Löf type theory
,
https://cs.stackexchange.com/questions/82810/reducing-products-in-hott-to-church-scott-encodings/82891#82891

ベストアンサー

あなたは類似しているが別個のいくつかの質問をしています。

  1. Why doesn’t the HoTT book use Church encodings for data
    types?

    Church encodings do not work in Martin-Löf type theory, for two
    reasons.

    First, MLTT is predicative. There is a universe
    hierarchy, and each type lives at a particular universe level, and
    a type at level $n$ can only quantify over types at smaller
    universe levels $k < n$. Church encodings like in System F or
    the CoC require impredicative quantification, where you
    can instantiate quantifiers with types which are the same size, or
    even bigger.

    Second, even if you defined datatypes like the natural numbers
    with Church encodings, to do proofs with these types, you need
    induction principles to prove things about them. To derive
    induction principles for Church encodings, you need to use an
    argument based on Reynolds’ parametricity, and the question of how
    to internalize parametricity principles into type theory is still
    not fully settled. (The state of the art is Nuyts, Vezzosi, and
    Devriese’s ICFP 2017 paper Parametric Quantifiers for Dependent
    Type Theory
    — note that this is well after the HoTT
    book was written!)

  2. Next, you are asking why the foundation is not minimal. This is
    actually one of the distinctive sociological features of
    type-theoretic foundations — type theorists regard having a small
    set of rules as a technical convenience, without much foundational
    significance. It’s far, far more important to have the
    right set of rules, rather than the smallest set
    of rules.

    We develop type theories to be used by
    mathematicians and programmers, and it’s very, very important that
    the proofs done within type theory are the ones that mathematicians
    and programmers regard as being done in the right way. This is
    because the arguments mathematicians typically regard as having
    good style typically are structured using the key algebraic and
    geometrical principles of the domain of study. If you have to use
    complicated encodings then much structure is lost or obscured.

    This is why even type-theoretic presentations of propositional
    classical logic invariably give all the logical connectives, even
    though it is formally equivalent to a logic with just NAND. Sure,
    all the boolean connectives can be encoded with NAND, but that
    encoding obscures the structure of the logic.

返信を残す

メールアドレスが公開されることはありません。 * が付いている欄は必須項目です