如何在CCG中用Lambda-Calculus定义相等谓词'are'？

给定如下CCG语法，需要为单词are定义正确的Lambda-Calculus表示，使其作为相等谓词，用于解析all logicians are linguists这类句子，但尝试的两种定义均出现问题：

ccg = '''
# CCG grammar
# complete the lexical entries with their categories and semantics

:- S, NP, N

logicians => NP { \\x. LOGICIANS(x) }
logicians => N { \\x. LOGICIANS(x) }
linguists => NP { \\x. LINGUISTS(x) }
linguists => N { \\x. LINGUISTS(x) }
engineers => NP { \\x. ENGINEERS(x) }
engineers => N { \\x. ENGINEERS(x) }

non => NP/N { \\N x. ~N(x) }

are => (S\\NP)/NP  {\\x y.are(x,y)}

all => NP/N { \\P Q. all x. (P(x) -> Q(x)) }
no => NP/N { \\P Q. all x. (P(x) -> ~Q(x)) }
some => NP/N { \\N V. exists x. (N(x) & V(x)) }
'''

尝试的定义及问题 #

• 第一种定义：

  are => (S\\NP)/NP {\\X x.X(\\y.are(x,y))}
  

  得到错误的语义解释：

  S {are(\\x.LINGUISTS(x),\\Q.all x.(LOGICIANS(x) -> Q(x)))}
  

• 第二种定义：

  are => (S\\NP)/NP { \\X Y. all y. (X(y) <-> Y(y)) }
  

  触发逻辑表达式错误：

  LogicalExpressionException: 'y' is an illegal predicate name.  Individual variables may not be used as predicates.
  all y.(LINGUISTS(y) <-> all x.(LOGICIANS(x) -> y(x)))
  

注：无法修改语法中的S、NP、N规则，需找到可行的Lambda定义方式。

要正确实现are作为谓词等价的连接词（对应句子中两个谓词外延相等的语义），需匹配CCG范畴(S\\NP)/NP对应的语义类型，以下是正确的Lambda定义：

正确定义 #

are => (S\\NP)/NP { \\P Q. all x. (Q(x) <-> P(x)) }

关键解释 #

1. 范畴与类型匹配：(S\\NP)/NP的语义类型为<<e,t>,<<e,t>,t>>，即接受两个一元谓词（类型<e,t>，对应NP的语义，比如LINGUISTS或all logicians对应的谓词），返回真值（类型t），该定义完全匹配此类型要求。
2. 语义逻辑对应：all x. (Q(x) <-> P(x))表示“对所有个体x，x满足Q当且仅当x满足P”，恰好对应“are”作为相等谓词的语义——两个谓词的外延完全重合。
3. 错误原因分析：
   • 第一种定义的语义结构与范畴不匹配，导致高阶谓词与个体谓词错误绑定，生成混乱的嵌套Lambda表达式。
   • 第二种定义的变量绑定顺序错误：CCG组合时Y会被绑定到all logicians对应的高阶谓词\\Q.all x.(LOGICIANS(x) -> Q(x))，而非一元谓词，进而导致Y(y)出现“用个体变量作为谓词”的类型违规，触发错误。

解析结果验证 #

用正确定义解析all logicians are linguists时，最终会得到语义：all x.(LOGICIANS(x) <-> LINGUISTS(x))，完全符合句子“所有逻辑学家等价于语言学家”的语义要求。

内容的提问来源于stack exchange，提问作者Julius