我正在研究Lambda微积分并且我坚持减少....可以用这个例子来解释减少的类型,特别是以最简单的方式减少beta.也不介意一个易于理解的教程.
(?xyz .xyz )(?x .xx )(?x .x )x
rp.beltran.. 93
Lambda演算
Lambda演算有一种循环进入许多步骤的方法,使得解决问题变得乏味,并且它看起来很难,但实际上并不是那么糟糕.在lambda演算中,只有lambdas,你可以用它们做的就是替换.Lambdas就像一个函数或方法 - 如果您熟悉编程,它们是将函数作为输入的函数,并返回一个新函数作为输出.
lambda演算中基本上有两个半的过程:1)Alpha转换 - 如果要在其中应用两个具有相同变量名的lambda表达式,则将其中一个更改为新的变量名.例如,(λx.xx)(λx.x)在缩小之后变为类似(λx.xx)(λy.y)或(λx.xx)(λx'.x').结果与您开始时的结果相同,只是使用不同的变量名称.
2)Beta减少 - 基本上只是替换.这是使用输入调用lambda表达式并获取输出的过程.lambda表达式就像一个函数,通过在整个表达式中替换输入来调用函数.取(λx.xy)z,(λx.xy)的后半部分,输出后的所有内容,输出,保持输出,但用提供的输入替换变量(在句点之前命名).z是输入,x是参数名称,xy是输出.发现在输出的参数的所有匹配,并与输入替换它们,这就是它减少到,所以(?x.xy)z=> xy与z取代x,这是zy.
2.5)Eta转换/ Eta减少 - 这是特殊情况减少,我只称之为半个过程,因为它有点降低Beta,有点,因为技术上它不是.您可能会看到它写在维基百科或教科书中,因为"每当x在f中没有出现时,Eta转换在λx.(fx)和f之间进行转换",这听起来真的很混乱.所有真正意味着是λx.(fx)= f如果f不使用x.如果它实际上是完全有意义的,但通过一个例子更好地显示.考虑(λx.(λy.yy)x),这相当于通过eta减少到(λy.yy),因为f =(λy.yy),其中没有x,你可以通过减少它来证明这一点,因为它将解决(λx.xx),这是显而易见的相同的事情.你说要专注于beta减少,所以我不打算在它应得的细节上讨论eta转换,但很多人在cs理论堆栈交换中放弃了它
关于Beta减少的符号:我将使用以下表示法将提供的输入替换为输出:
(? param . output)input=> output [param := input]=>result
这意味着我们在输出中替换param的出现,这就是它减少到的结果
例:
(?x.xy)z
= (xy)[x:=z]
= (zy)
= zy
您提出的问题只能通过Alpha转换和Beta降低来解决,请不要被以下过程的持续时间所吓倒.毫无疑问,这很长,但解决它的任何步骤都不是很难.
(λxyz.xyz)(λx.xx)(λx.x)x
=(((λxyz.xyz)(λx.xx))(λx.x))x - 让我们在"正常顺序"中添加括号,左侧相关性,abc减少为((ab)c),其中b应用于a和c应用于其结果
=(((λxyz.xyz)(λx.xx))(λx.x))x - 选择最深的嵌套应用程序并首先减少它.
粗体部分减少为:
(λxyz.xyz)(λx.xx)
=(λx.λyz.xyz)(λx.xx) - 意思相同,但是我们拉出第一个参数,因为我们要将它减少,所以我希望它清楚
=(λx.λyz.xyz)(λx'.x'x') - Alpha转换,有些人坚持使用新字母,但我喜欢在末尾附加数字或者s,两种方式都可以.因为两个表达式都使用参数x,所以我们必须在一侧重命名它们,因为两个X是局部变量,所以不必表示相同的东西.
=(λyz.xyz)[x:=λx'.x'x'] - beta减少的符号,我们删除第一个参数,并用输出的内容替换它在输出中的出现次数[a:= b]表示a将被替换为b.
=(λyz.(λx'.x'x')yz) - 实际的减少,我们用提供的lambda表达式替换x的出现.
=(λyz.((λx'.x'x')y) z) - 再次为括号的正常顺序,并且看,另一个应用程序要减少,这个时间y应用于(xλxx`),所以让我们现在减少
=(λyz.((x'x')[x':= y]) z) - 将其放入β减少符号中.
=(λyz.(yy) z) - 我们将两次出现的x'x'交换为Ys,现在完全减少了.
将其添加回原始表达式:
(((λxyz.xyz)(λx.xx))(λx.x))x
=((λyz.(yy)z)(λx.x))x - 这不是新的,只是把我们之前发现的东西放回去.
=((λyz.(yy)z)(λx.x))x - 抓取最深的嵌套应用程序,将(λx.x)应用于(λyz.(yy)z)
我们将再次单独解决这个问题:
(λyz.(YY)Z)(λx.x)
=(λy.λz.(yy)z)(λx.x) - 为了清晰起见,只需将第一个参数输出.
=(λz.(yy)z)[y:=(λx.x)] - 加入beta减法表示法,我们弹出第一个参数,并注意Ys将被切换为(λx.x)
=(λz.((λx.x )(λx.x))z) - 实际减少/替换,现在可以减少粗体部分
=(λz.((x)[x:=λx.x])z) - 希望你现在得到的图片,我们开始通过将它放入表格来减少(λx.x)(λx.x) (x)[x:=λx.x]
=(λz.((λx.x ))z) - 并且存在替换
=(λz.(λx.x )z) - 清除了过多的括号,我们发现了什么,但另一个应用程序要处理
=(λz.(x)[x:= z]) - 弹出x参数,放入符号
=(λz.(z)) - 执行替换
=(λz.z) - 清除过多的括号
把它放回主表达式:
((λyz.(yy)z)(λx.x))x
=((λz.z))x - 填写我们上面证实的内容
=(λz.z)x - 清除过多的括号,现在减少到最后一个应用,x应用于(λz.z)
=(z)[z:= x] - β减少,加入符号
=(x) - 进行替换
= x - 清除过多的括号
是的.答案是z,它减少了只是常规.
Lambda演算有一种循环进入许多步骤的方法,使得解决问题变得乏味,并且它看起来很难,但实际上并不是那么糟糕.在lambda演算中,只有lambdas,你可以用它们做的就是替换.Lambdas就像一个函数或方法 - 如果您熟悉编程,它们是将函数作为输入的函数,并返回一个新函数作为输出.
lambda演算中基本上有两个半的过程:1)Alpha转换 - 如果要在其中应用两个具有相同变量名的lambda表达式,则将其中一个更改为新的变量名.例如,(λx.xx)(λx.x)在缩小之后变为类似(λx.xx)(λy.y)或(λx.xx)(λx'.x').结果与您开始时的结果相同,只是使用不同的变量名称.
2)Beta减少 - 基本上只是替换.这是使用输入调用lambda表达式并获取输出的过程.lambda表达式就像一个函数,通过在整个表达式中替换输入来调用函数.取(λx.xy)z,(λx.xy)的后半部分,输出后的所有内容,输出,保持输出,但用提供的输入替换变量(在句点之前命名).z是输入,x是参数名称,xy是输出.发现在输出的参数的所有匹配,并与输入替换它们,这就是它减少到,所以(?x.xy)z=> xy与z取代x,这是zy.
2.5)Eta转换/ Eta减少 - 这是特殊情况减少,我只称之为半个过程,因为它有点降低Beta,有点,因为技术上它不是.您可能会看到它写在维基百科或教科书中,因为"每当x在f中没有出现时,Eta转换在λx.(fx)和f之间进行转换",这听起来真的很混乱.所有真正意味着是λx.(fx)= f如果f不使用x.如果它实际上是完全有意义的,但通过一个例子更好地显示.考虑(λx.(λy.yy)x),这相当于通过eta减少到(λy.yy),因为f =(λy.yy),其中没有x,你可以通过减少它来证明这一点,因为它将解决(λx.xx),这是显而易见的相同的事情.你说要专注于beta减少,所以我不打算在它应得的细节上讨论eta转换,但很多人在cs理论堆栈交换中放弃了它
关于Beta减少的符号:我将使用以下表示法将提供的输入替换为输出:
(? param . output)input=> output [param := input]=>result
这意味着我们在输出中替换param的出现,这就是它减少到的结果
例:
(?x.xy)z
= (xy)[x:=z]
= (zy)
= zy
您提出的问题只能通过Alpha转换和Beta降低来解决,请不要被以下过程的持续时间所吓倒.毫无疑问,这很长,但解决它的任何步骤都不是很难.
(λxyz.xyz)(λx.xx)(λx.x)x
=(((λxyz.xyz)(λx.xx))(λx.x))x - 让我们在"正常顺序"中添加括号,左侧相关性,abc减少为((ab)c),其中b应用于a和c应用于其结果
=(((λxyz.xyz)(λx.xx))(λx.x))x - 选择最深的嵌套应用程序并首先减少它.
粗体部分减少为:
(λxyz.xyz)(λx.xx)
=(λx.λyz.xyz)(λx.xx) - 意思相同,但是我们拉出第一个参数,因为我们要将它减少,所以我希望它清楚
=(λx.λyz.xyz)(λx'.x'x') - Alpha转换,有些人坚持使用新字母,但我喜欢在末尾附加数字或者s,两种方式都可以.因为两个表达式都使用参数x,所以我们必须在一侧重命名它们,因为两个X是局部变量,所以不必表示相同的东西.
=(λyz.xyz)[x:=λx'.x'x'] - beta减少的符号,我们删除第一个参数,并用输出的内容替换它在输出中的出现次数[a:= b]表示a将被替换为b.
=(λyz.(λx'.x'x')yz) - 实际的减少,我们用提供的lambda表达式替换x的出现.
=(λyz.((λx'.x'x')y) z) - 再次为括号的正常顺序,并且看,另一个应用程序要减少,这个时间y应用于(xλxx`),所以让我们现在减少
=(λyz.((x'x')[x':= y]) z) - 将其放入β减少符号中.
=(λyz.(yy) z) - 我们将两次出现的x'x'交换为Ys,现在完全减少了.
将其添加回原始表达式:
(((λxyz.xyz)(λx.xx))(λx.x))x
=((λyz.(yy)z)(λx.x))x - 这不是新的,只是把我们之前发现的东西放回去.
=((λyz.(yy)z)(λx.x))x - 抓取最深的嵌套应用程序,将(λx.x)应用于(λyz.(yy)z)
我们将再次单独解决这个问题:
(λyz.(YY)Z)(λx.x)
=(λy.λz.(yy)z)(λx.x) - 为了清晰起见,只需将第一个参数输出.
=(λz.(yy)z)[y:=(λx.x)] - 加入beta减法表示法,我们弹出第一个参数,并注意Ys将被切换为(λx.x)
=(λz.((λx.x )(λx.x))z) - 实际减少/替换,现在可以减少粗体部分
=(λz.((x)[x:=λx.x])z) - 希望你现在得到的图片,我们开始通过将它放入表格来减少(λx.x)(λx.x) (x)[x:=λx.x]
=(λz.((λx.x ))z) - 并且存在替换
=(λz.(λx.x )z) - 清除了过多的括号,我们发现了什么,但另一个应用程序要处理
=(λz.(x)[x:= z]) - 弹出x参数,放入符号
=(λz.(z)) - 执行替换
=(λz.z) - 清除过多的括号
把它放回主表达式:
((λyz.(yy)z)(λx.x))x
=((λz.z))x - 填写我们上面证实的内容
=(λz.z)x - 清除过多的括号,现在减少到最后一个应用,x应用于(λz.z)
=(z)[z:= x] - β减少,加入符号
=(x) - 进行替换
= x - 清除过多的括号
是的.答案是z,它减少了只是常规.
京公网安备 11010802040832号 | 京ICP备19059560号-6 