5

我正在尝试为这个语法编写一个具体的语法（来自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 的更多操作？

4

1 回答 1

2

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

注意区别：

介绍Ints n：一个参数类型

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

-- from the Finnish resource grammar
oper
  NForms : Type = Predef.Ints 10 => Str ;

  nForms10 : (x1,_,_,_,_,_,_,_,_,x10 : Str) -> NForms =
    \ukko,ukon,ukkoa,ukkona,ukkoon,
       ukkojen,ukkoja,ukkoina,ukoissa,ukkoihin -> table {
    0 => ukko ;   1 => ukon ;    2 => ukkoa ;
    3 => ukkona ; 4 => ukkoon ;  5 => ukkojen ;
    6 => ukkoja ; 7 => ukkoina ; 8 => ukoissa ;
    9 => ukkoihin ; 10 => ukko
    } ;

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

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

-- another way to write the example from the Finnish RG
param
  NForm = SgNom | SgGen | … | PlGen | PlIll ; -- Named params instead of Ints 10
oper
  NForms : Type = NForm => Str ;

  nForms10 : (x1,_,_,_,_,_,_,_,_,x10 : Str) -> NForms =
    \ukko,ukon,ukkoa,ukkona,ukkoon,
       ukkojen,ukkoja,ukkoina,ukoissa,ukkoihin -> table {
    SgNom => ukko ; 
    SgGen => ukon ;
    ...
    PlGen => ukkojen ;
    PlIll => ukkoihin
    } ;

如您所见，整数用作列表的左侧：5 => ukkojen与 GF 一样有效PlGen => ukkojen。在那种特殊情况下，5具有 type Ints 10。

无论如何，该代码只是为了向您Ints n展示它是什么以及它如何在我的其他语法中使用，我将很快将其粘贴在这里。

第 1 步：递增 Int

最初，我想Int在我的 lincat 中用作Nat. 但现在我将使用它Ints 100。我线性Zero化为{n = 0}.

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

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

  lin
    Succ x = {n = myPlus1 ! x.n} ;

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

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

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

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

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

$ gf
…

> i -retain ArithmC.gf 

> cc Zero
{n = 0; lock_Nat = <>}

> cc Succ Zero
{n = 1; lock_Nat = <>}

> cc Succ (Succ (Succ (Succ (Succ Zero))))
{n = 5; lock_Nat = <>}

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

第2步：把它Ints n变成一个NP

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

Int（和所有文字类型）的 lincat是{s : Str}. 要将文字变成 a NP，您可以使用Symbolic 模块。

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

但是没有 lincat for Ints n，因为它是一个param. 所以我发现的唯一方法是手动showNat为Ints 100.

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

concrete ArithmEng of Arithm =
  open Predef, SymbolicEng, SyntaxEng, ParadigmsEng in {
  lincat
    Prop = S ;
    Nat  = {s : NP ; n : MyInts} ;
  oper
    MyInts = Ints 100 ;
  lin
    Zero     = mkNat 0 ;
    Succ nat = mkNat (myPlus1 ! nat.n) ;
    Even nat = mkS (mkCl nat.s (mkA "even")) ;
    And p q  = mkS and_Conj p q ;
  oper
    mkNat : MyInts -> Nat ;
    mkNat i = lin Nat {s = symb (showNat ! i) ; n = i} ;

    myPlus1 : MyInts => MyInts = table {
      100 => 100 ;
      n => Predef.plus n 1
      } ;

    showNat : MyInts => Str ;
    showNat = table {
      0 => "0" ; 1 => "1" ; 2 => "2" ;
      3 => "3" ; 4 => "4" ; 5 => "5" ;
      6 => "6" ; 7 => "7" ; 8 => "8" ;
      9 => "9" ; 10 => "10" ; 11 => "11" ;
      12 => "12" ; 13 => "13" ; 14 => "14" ;
      15 => "15" ; 16 => "16" ; 17 => "17" ;
      18 => "18" ; 19 => "19" ; 20 => "20" ;
      _ => "Too big number, I can't be bothered"
      } ;
} ;

让我们在 GF shell 中测试：

Arithm> gr | l -treebank
Arithm: Even (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))
ArithmEng: 12 is even

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

其他解决方案

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

于 2021-03-16T10:30:53.227 回答