标签: lambda-calculus

我正在看教程http://haskell.org/haskellwiki/How_to_write_a_Haskell_program

import System.Environment

main :: IO ()
main = getArgs >>= print . haqify . head

haqify s = "Haq! " ++ s

在HLint下运行此程序时,它会出现以下错误;

./Haq.hs:11:1: Warning: Eta reduce
Found:
  haqify s = "Haq! " ++ s
Why not:
  haqify = ("Haq! " ++ )

有人能否对"Eta Reduce"在这种背景下意味着什么有所了解？

我有一个有趣的问题,但我不确定如何用它来表达...

考虑lambda演算.对于给定的lambda表达式,有几种可能的缩减顺序.但其中一些不会终止,而另一些则会终止.

在lambda演算中,事实证明存在一个特定的减少顺序,如果实际存在,则保证总是以不可简化的解决方案终止.它被称为正常秩序.

我写了一个简单的逻辑解算器.但麻烦的是,它处理约束的顺序似乎对它是否找到任何解决方案产生了巨大影响.基本上,我想知道我的逻辑编程语言是否存在类似正常顺序的东西.(或者说,单纯的机器无法确定地解决这个问题.)

这就是我所追求的.据推测,答案关键取决于"简单逻辑解算器"到底是什么.所以我将尝试简要描述一下.

我的节目紧密地基于编程乐趣(Jeremy Gibbons&Oege de Moor)第9章中的组合系统.该语言具有以下结构:

• 求解器的输入是单个谓词.谓词可能涉及变量.求解器的输出为零或更多解.解决方案是一组变量赋值,它使谓词成为正确.

• 变量持有表达式.表达式是整数,变量名或子表达式的元组.

• 有一个等式谓词,用于比较表达式(不是谓词)的相等性.如果用其值替换每个(绑定)变量使两个表达式相同,则会感到满意.(特别是,每个变量都等于它自己,绑定与否.)这个谓词是使用统一来解决的.

• 还有AND和OR的运算符,它们以明显的方式工作.没有NOT运算符.

• 有一个"存在"运算符,它基本上创建局部变量.

• 定义命名谓词的工具支持递归循环.

关于逻辑编程的一个"有趣的事情"是,一旦你编写了一个命名谓词,它通常会向前和向后(有时甚至是横向).典型示例:用于连接两个列表的谓词也可用于将列表拆分为所有可能的对.

但有时向后运行谓词会导致无限搜索,除非您重新排列术语的顺序.(例如,交换一个AND的LHS和RHS或者一些OR.)我想知道是否有一些自动方法来检测运行谓词的最佳顺序,以确保在解决方案集完全正确的所有情况下立即终止有限.

有什么建议？

通过查看代码而不是阅读冗长的解释,我更喜欢学习.这可能是我不喜欢长篇学术论文的原因之一.代码是明确的,紧凑的,无噪音的,如果你没有得到的东西,你可以玩它 - 不需要问作者.

这是Lambda微积分的完整定义:

-- A Lambda Calculus term is a function, an application or a variable.
data Term = Lam Term | App Term Term | Var Int deriving (Show,Eq,Ord)

-- Reduces lambda term to its normal form.
reduce :: Term -> Term
reduce (Var index)      = Var index
reduce (Lam body)       = Lam (reduce body)
reduce (App left right) = case reduce left of
    Lam body  -> reduce (substitute (reduce right) body)
    otherwise -> App (reduce left) (reduce …

我无法理解维基百科上给出的HM系统的letrec定义,这里:https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system#Recursive_definitions

对我来说,规则大致转换为以下算法:

1. 推断letrec定义部分中 所有内容的类型
   1. 为每个定义的标识符分配临时类型变量
   2. 使用临时类型递归处理所有定义
   3. 成对,将结果与原始临时变量统一起来
2. close(with forall)推断类型,将它们添加到基础(context)并用它推断表达式部分的类型

我遇到这样的程序有问题:

letrec
 p = (+)     --has type Uint -> Uint -> Uint
 x = (letrec
       test = p 5 5
     in test)
in x

我观察的行为如下:

• p获取临时类型的定义a
• x获取一些临时类型的定义,但现在超出了我们的范围
• in x,test获取临时类型的定义t
• pa从范围中获取临时类型,使用HM规则作为变量
• (f 5)得到由HM规则应用,造成类型是处理b(以及(统一a与结合Uint -> b)
• ((p 5) 5)由同一规则处理,导致更多的统一和类型c,a现在结果统一Uint -> Uint -> c
• 现在,测试关闭以输入 forall …

当我在这里阅读Church Rosser II定理时

定理(Church Rosser II)

如果有一个终止减少,那么最外面的减少也将终止.

我想知道:是否有一些定理加强了教会Rosser II定理,以便它告诉渐近时间复杂度而不是终止？

或者,是否可以证明所需减少策略在所有减少策略中具有最小的渐近时间复杂度？

我正在尝试围绕 lambda 演算，以及它与语言、编译器和二进制代码的关系。lambda 演算等同于图灵机的实际含义是什么，它实际上在哪里表现出来？

我不明白 lambda 演算如何取代图灵机作为计算的理论模型。图灵机是关于改变状态的顺序指令，lambda 演算是关于对某些东西进行评估的表达式。它更抽象，就像它自己的编程语言，而不是如何实际计算某些东西、使事情发生的模型。或者让我们这样说：lambda 演算就像路线图，而图灵机就像汽车模型。这两个如何被认为是等价的？是否有可能在不实施图灵机的情况下在硬件上运行软件？

例如，lisp 编译器和语言如何与 lambda 演算相关？lambda演算在哪一层实现？就 lambda 演算的定义而言，实现是否纯粹？lambda 演算背后的理论在哪里以及如何将语法转换为正在运行的二进制文件？例如，在 lambda 演算中，数字被编码为应用于其他函数 n 次的特殊函数。然而在语法上，我们使用数字文字。所有这些公理在哪里使用？

从这篇Haskell Cafe 帖子中，并借用jyp的一些代码示例，我们可以在 Haskell 中构造一个简单的 PHOAS 求值器，如下所示：

{-# LANGUAGE GADTs #-}\n{-# LANGUAGE RankNTypes #-}\n\nimport Data.Char\n\ndata Term v t where\n   Var :: v t -> Term v t\n   App :: Term v (a -> b) -> Term v a -> Term v b\n   Lam :: (v a -> Term v b) -> Term v (a -> b)\n\ndata Exp t = Exp (forall v. Term v t)\n\n-- An evaluator\neval :: Exp t -> t\neval (Exp e) = …

我正在为纯功能程序开发虚拟机,我希望能够测试和使用已有的各种Haskell模块.VM在无类型lambda演算中基本上作为输入.我想知道从现代Haskell模块中提取这样一个表示的好方法(例如,使用MPTC,模式保护等).我做了一点研究,似乎没有一个工具可以做到这一点(我会很高兴被误解),这没关系.我正在寻找一种方法.

GHC Core似乎过于注重操作,特别是因为VM所做的一件事就是显着改变评估顺序.是否有任何可访问的中间表示更接近于lambda演算？

我正在尝试使用以下方法建立减法,加法,除法,乘法和其他操作:

1. incr(x) - 一旦调用此函数,它将x + 1分配给x
2. assign(x,y) - 此函数将y的值赋给x(x = y)
3. 零(x) - 此函数将0分配给x(x = 0)
4. 循环X {} - 括号内的操作将执行X次

使用以下规则,可以直接实现这样的添加(添加):

ADD (x, y) {
 loop X {
   y = incr (y)
 }
return y
}

但是,我正在努力实现减法.我认为所有其他所需的操作都可以使用减法完成.

任何提示都将非常感激.

在系统F中,类型exists a. P可以被编码为forall b. (forall a. P -> b) -> b使用存在性的任何系统F术语可以根据关于打字和缩减规则的该编码来表达.

在"类型和编程语言"中,将显示以下练习:

我们可以根据存在类型编码通用类型吗？

我的直觉说这是不可能的,因为在某种程度上,"存在包装"机制并不像"类型抽象"机制那样强大.我如何正式展示这个？

我甚至不确定我需要证明什么才能正式显示这个结果.