Lambda Calculus 中的pair/vireo 访问如何工作？答案

【问题标题】：How does pair/vireo accessing work in Lambda Calculus?Lambda Calculus 中的pair/vireo 访问如何工作？
【发布时间】：2021-03-18 17:38:20
【问题描述】：

（免责声明语法：我使用的是 λ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 === ?

如您所见，我不知道是否可以从λa 访问t(type)，即使您将列表/对数据结构传递给它。如果这不起作用，为什么？什么会？

【问题讨论】：

标签： lambda lambda-calculus

【解决方案1】：

我意识到这是无效的，因为我只是将 a 作为参数应用。

这样做的方法是为数据结构定义我们自己的选择器。

fst:= λabcd.a snd:= λabcd.b 等等......最好我们可以使用教堂数字。

选择器：= λnabcd.EQnN1 a EQnN2 b EQnN3 c EQnN4 d

所以在我们的绑定函数中： λab.AND is0(K(selectorN4a) KI(selectorN4b)) Covalentab...等等。

可能有更好的方法来做到这一点，但我现在不知道。

【讨论】：