问题描述
（免责声明语法：我使用 λabc.exp 而不是 λa.λb.λc.exp）
TLDR/更简单的示例：
V:= λgxf.f(ga)
GETG:= λa.a(g)
GETG V(N1 N2)
我想知道这是否有效，即。 GETG === N1
FULL（我实际上在做什么）： 我做了一个小化学模型，我的目标是能够在函数中使用我的数据结构。
V:= λgxf.f(gx)
ELEMENT:= λpnetf.f(pnet)
BONDDATA:= λab.Vab
NONMetaL:= V(N0 N0)
MetaL:= V(N1 N1)
请注意，我为一对/vireo 数据制作了一个列表。
（对ELEMENT的参数有好奇的人输入如下：proton,neutron,electron,type）
现在我将定义我的绑定函数和元素：
HYDROGEN:= ELEMENT(N1 N0 N1 NONMetaL)
H-PAIR:= BONDDATA(HYDROGEN HYDROGEN)
CovalENT:= ...placeholder
IONIC:= ...placeholder
BOND:= λab.a(AND is0(t(a)) is0(t(b))) b(AND is0(t(a)) is0(t(b)))CovalENTab IONICab
BOND H-PAIR === ?
如您所见，即使您将列表/对数据结构传递给它，我也不知道是否可以从 t 访问 λa(type)。如果这不起作用，为什么？什么会？
解决方法
我意识到这是无效的，因为我只是将 a 作为参数应用。
这样做的方法是为数据结构定义我们自己的选择器。
fst:= λabcd.a snd:= λabcd.b 等等......最好我们可以使用教堂数字。
选择器：= λnabcd.EQnN1 a EQnN2 b EQnN3 c EQnN4 d
所以在我们的债券函数中： λab.AND is0(K(selectorN4a) KI(selectorN4b)) Covalentab...等等。
可能有更好的方法来做到这一点，但我现在不知道。