语法框架：“线性化类型字段不能为 Int”；如何使用算术表达式为语法编写具体的语法？

Question

我正在尝试为此语法编写具体的语法（来自Grammatical Framework: Programming with Multilingual Grammars 的第 6 章）：

abstract Arithm = {
  flags startcat = Prop ;
  cat
    Prop ;                        -- proposition
    Nat ;                         -- natural number
  fun
    Zero : Nat ;                  -- 0
    Succ : Nat -> Nat ;           -- the successor of x
    Even : Nat -> Prop ;          -- x is even
    And  : Prop -> Prop -> Prop ; -- A and B
}

整数、浮点数和字符串文字（Int、Float和String）有预定义的类别，它们可以用作函数的参数，但它们可能不是任何函数的值类型。

此外，它们不能用作线性化类型中的字段。这就是我想要做的，使用plus 在 Predef.gf 中定义：

concrete ArithmEng of Arithm =
  open Predef, SymbolicEng, SyntaxEng, ParadigmsEng in
  lincat
    Prop = S ;
    Nat  = {s : NP ; n : Int} ;
  lin
    Zero     = mkNat 0 ;
    Succ nat = let n' : Int = Predef.plus nat.n 1 in mkNat n' ;
    Even nat = mkS (mkCl nat.s (mkA "even")) ;
    And p q  = mkS and_Conj p q ;
  oper
    mkNat  : Int -> Nat ;
    mkNat int = lin Nat {s = symb int ; n = int} ;
} ;

但当然，这不起作用：我收到错误“线性化类型字段不能为 Int”。

也许我的问题的正确答案是使用另一种编程语言，但我很好奇，因为这个例子在 GF 书中留给读者作为练习，所以我希望它是可以解决的。

我可以写一元的解决方案，使用类别Digits来自Numeral.gf：

concrete ArithmEng of Arithm =
  open SyntaxEng, ParadigmsEng, NumeralEng, SymbolicEng, Prelude in {
  lincat
    Prop = S ;
    Nat = {s : NP ; d : Digits ; isZero : Bool} ;
  lin
    Zero = {s = mkNP (mkN "zero") ; d = IDig D_0 ; isZero = True} ;
    Succ nat = case nat.isZero of {
                 True  => mkNat (IDig D_1) ;
                 False => mkNat (IIDig D_1 nat.d) } ;
    Even nat = mkS (mkCl nat.s (mkA "even")) ;
    And p q  = mkS and_Conj p q ;
  oper
    mkNat : Digits -> Nat ;
    mkNat digs = lin Nat {s = symb (mkN "number") digs ; d = digs ; isZero = False} ;
} ;

这会产生以下结果：

Arithm> l -bind Even Zero
zero is even

0 msec
Arithm> l -bind Even (Succ Zero)
number 1 is even

0 msec
Arithm> l -bind Even (Succ (Succ (Succ Zero)))
number 111 is even

这当然是一个可能的答案，但我怀疑这不是该练习旨在解决的方式。所以我想知道我是否遗漏了什么，或者GF语言是否曾经支持对Ints的更多操作？

Answer 1

一个可能但仍然不太令人满意的答案是使用Ints n任何自然数的参数n。

\n

注意区别：

\n

\n
• Int是文字类型，就像Stringand一样Float。
\n
• 所有文字在每个具体语法中都有{s : Str}其 lincat，并且您不能以任何方式更改它。
\n
• 由于 lincat 包含Str（不是 String），因此不允许您在运行时对其进行模式匹配。
\n

\n

介绍Ints n：参数类型

\n

然而，Ints n是一个参数类型，因为它是有限的。\n您可能在旧的 RGL 语言中见过Ints n，如以下芬兰语语法：

\n

-- from the Finnish resource grammar\noper\n  NForms : Type = Predef.Ints 10 => Str ;\n\n  nForms10 : (x1,_,_,_,_,_,_,_,_,x10 : Str) -> NForms =\n    \\ukko,ukon,ukkoa,ukkona,ukkoon,\n       ukkojen,ukkoja,ukkoina,ukoissa,ukkoihin -> table {\n    0 => ukko ;   1 => ukon ;    2 => ukkoa ;\n    3 => ukkona ; 4 => ukkoon ;  5 => ukkojen ;\n    6 => ukkoja ; 7 => ukkoina ; 8 => ukoissa ;\n    9 => ukkoihin ; 10 => ukko\n    } ;\n

\n

这里发生了什么事？这是一个变形表，其中左侧 \xe2\x80\xa6 只是数字，而不是大小写和数字的组合。（例如，5对应于复数属格。是的，对于没有编写该语法的人来说，它是完全无法阅读的。）

\n

同样的代码也可以这样写：

\n

-- another way to write the example from the Finnish RG\nparam\n  NForm = SgNom | SgGen | \xe2\x80\xa6 | PlGen | PlIll ; -- Named params instead of Ints 10\noper\n  NForms : Type = NForm => Str ;\n\n  nForms10 : (x1,_,_,_,_,_,_,_,_,x10 : Str) -> NForms =\n    \\ukko,ukon,ukkoa,ukkona,ukkoon,\n       ukkojen,ukkoja,ukkoina,ukoissa,ukkoihin -> table {\n    SgNom => ukko ; \n    SgGen => ukon ;\n    ...\n    PlGen => ukkojen ;\n    PlIll => ukkoihin\n    } ;\n

\n

正如您所看到的，整数作为列表的左侧：5 => ukkojen与 GF 一样有效PlGen => ukkojen。在该特定情况下，5具有类型Ints 10.

\n

不管怎样，该代码只是为了向您展示它Ints n是什么以及它如何在除我的语法之外的其他语法中使用，我很快就会将其粘贴到此处。

\n

第 1 步：递增 Int

\n

最初，我想用作Intlincat for 中的字段Nat。但现在我会用它Ints 100来代替。我线性Zero化为{n = 0}.

\n

concrete ArithmC of Arithm = open Predef in {\n  lincat\n    Nat = {n : Ints 100} ;\n  lin\n    Zero = {n = 0} ; -- the 0 is of type Ints 100, not Int!\n

\n

现在我们也线性化Succ。这是令人兴奋的消息：我们可以使用Predef.plus运行时值，因为运行时值不再是Int，而是Ints n——这是有限的！所以我们可以这样做：

\n

  lin\n    Succ x = {n = myPlus1 ! x.n} ;\n\n  oper\n    -- We use Predef.plus on Ints 100, not Int\n    myPlus1 : Ints 100 => Ints 100 = table {\n      100 => 100 ;           -- Without this line, we get error\n      n => Predef.plus n 1   -- magic!\n      } ;\n}\n

\n

正如您从 中看到的myPlus1，绝对可以Ints n在运行时进行模式匹配。我们甚至可以使用它Predef.plus，只不过我们必须将其限制在最高值。如果没有该行100 => 100，我们会收到以下错误：

\n

- compiling ArithmC.gf... Internal error in GeneratePMCFG:\n    convertTbl: missing value 101\n                among 0\n                      1\n                      ...\n                      100\n

\n

不幸的是，它仅限于有限的n。

\n

让我们在 GF shell 中测试一下：

\n

$ gf\n\xe2\x80\xa6\n\n> i -retain ArithmC.gf \n\n> cc Zero\n{n = 0; lock_Nat = <>}\n\n> cc Succ Zero\n{n = 1; lock_Nat = <>}\n\n> cc Succ (Succ (Succ (Succ (Succ Zero))))\n{n = 5; lock_Nat = <>}\n

\n

如果你能这么说的话，从技术上讲是可行的。但我们还不能用它做任何有趣的事情。

\n

步骤 2：将Ints n变成NP

\n

cc之前，我们只是使用( compute_concrete )检查 GF shell 中的值。但语法的全部任务是生成像“2 是偶数”这样的句子。

\n

Int（以及所有文字类型）的 lincat是{s : Str}. 要将文字转换为 a NP，只需使用Symbolic 模块即可。

\n

但我们不能在运行时增加 an Int，所以我们选择使用 use Ints 100。

\n

但没有 lincat Ints n，因为它是param。所以我发现的唯一方法是手动定义一个showNat操作符Ints 100。

\n

这很丑陋，但从技术上讲它是有效的。

\n

- compiling ArithmC.gf... Internal error in GeneratePMCFG:\n    convertTbl: missing value 101\n                among 0\n                      1\n                      ...\n                      100\n

\n

让我们在 GF shell 中测试一下：

\n

Arithm> gr | l -treebank\nArithm: Even (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))\nArithmEng: 12 is even\n

\n

所以，是的，从技术上讲它是有效的，但它并不令人满意。它只适用于有限的n，我必须在操作中输入一堆样板文件showNat。我仍然不确定这是否是 GF 书中的预期方式，或者 GF 是否用于支持 Int 上的更多操作。

\n

其他解决方案

\n

这是daherb 的解决方案，其中Zero输出 string"0"并Succ输出 string "+1"，最后的输出用外部编程语言进行评估。

\n