Documentation

Linglib.Data.Treebank.Coverage.Schema

Treebank coverage of non-projectivity constraints: schema #

Typed schema for the per-treebank statistics a paper reports on how many of a treebank's dependency trees, or of the grammar rules extracted from them, satisfy a constraint on non-projectivity: projectivity, a bound on the gap degree or the edge degree, well-nestedness, planarity, or a conjunction of these. Generated rows live in Data/Treebank/Coverage/<Paper>.lean, emitted from the canonical <Paper>.json by scripts/gen_treebank_coverage.py.

This is data: it imports nothing from Linglib/ and states no theorems. A row records the covered quantity at the precision the paper prints, either as a count or as a percentage in hundredths, so that consumers compute over it by decide; Row.coverage is the common rational reading. The language code is a Glottolog code, an annotation for cross-study joins rather than a printed value.

References #

source
inductive Data.Treebank.Coverage.Constraint :
Type

A constraint on non-projectivity whose coverage a paper measures.

  • projective : Constraint

    Projectivity: gap degree 0, block-degree 1, fan-out 1.

  • gapDegreeEq (k : ℕ) : Constraint

    Gap degree exactly k.

  • gapDegreeLe (k : ℕ) : Constraint

    Gap degree at most k, block-degree and fan-out at most k + 1.

  • edgeDegreeEq (k : ℕ) : Constraint

    Edge degree exactly k.

  • wellNested : Constraint

    Well-nestedness.

  • planar : Constraint

    Planarity.

  • gapDegreeLeWellNested (k : ℕ) : Constraint

    Gap degree at most k together with well-nestedness.

Instances For
    source
    def Data.Treebank.Coverage.instDecidableEqConstraint.decEq (x✝ x✝¹ : Constraint) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      @[instance_reducible]
      instance Data.Treebank.Coverage.instDecidableEqConstraint :
      DecidableEq Constraint
      Equations
      source
      @[instance_reducible]
      instance Data.Treebank.Coverage.instReprConstraint :
      Repr Constraint
      Equations
      source
      def Data.Treebank.Coverage.instReprConstraint.repr :
      Constraint → ℕ → Std.Format
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        inductive Data.Treebank.Coverage.Item :
        Type

        What the coverage counts.

        • trees : Item

          Dependency trees of the treebank.

        • rules : Item

          Grammar rules extracted from the treebank, counted as tokens.

        Instances For
          source
          @[instance_reducible]
          instance Data.Treebank.Coverage.instDecidableEqItem :
          DecidableEq Item
          Equations
          source
          def Data.Treebank.Coverage.instReprItem.repr :
          Item → ℕ → Std.Format
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[instance_reducible]
            instance Data.Treebank.Coverage.instReprItem :
            Repr Item
            Equations
            source
            inductive Data.Treebank.Coverage.Scale :
            Type

            How the paper prints the covered quantity.

            • count : Scale

              A count of covered items.

            • percentHundredths : Scale

              A percentage of the total, in hundredths of a percent.

            Instances For
              source
              @[instance_reducible]
              instance Data.Treebank.Coverage.instDecidableEqScale :
              DecidableEq Scale
              Equations
              source
              def Data.Treebank.Coverage.instReprScale.repr :
              Scale → ℕ → Std.Format
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                @[instance_reducible]
                instance Data.Treebank.Coverage.instReprScale :
                Repr Scale
                Equations
                source
                structure Data.Treebank.Coverage.Row :
                Type

                One treebank's coverage under one constraint.

                • treebank : String

                  The treebank or language name as the paper prints it.

                • language : String

                  The Glottolog code of the treebank's language.

                • item : Item

                  What is counted.

                • total : ℕ

                  The number of items in the treebank.

                • constraint : Constraint

                  The constraint.

                • scale : Scale

                  The scale of value.

                • value : ℕ

                  The covered quantity at the paper's scale.

                Instances For
                  source
                  @[instance_reducible]
                  instance Data.Treebank.Coverage.instDecidableEqRow :
                  DecidableEq Row
                  Equations
                  source
                  def Data.Treebank.Coverage.instDecidableEqRow.decEq (x✝ x✝¹ : Row) :
                  Decidable (x✝ = x✝¹)
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    @[instance_reducible]
                    instance Data.Treebank.Coverage.instReprRow :
                    Repr Row
                    Equations
                    source
                    def Data.Treebank.Coverage.instReprRow.repr :
                    Row → ℕ → Std.Format
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      def Data.Treebank.Coverage.Row.coverage (r : Row) :
                      ℚ

                      The covered proportion of the treebank.

                      Equations
                      Instances For