标签: lambda-calculus

我应该采取这个代码:

f x y z = x^3 - g (x + g (y - g z) + g (z^2))
 where g x = 2*x^2 + 10*x + 1

并在没有(或让)的情况下重写它.

他们的意思是用Lambda函数写它(\ x - > ...)

我正在尝试在Haskell上重用Lambda函数.有任何想法吗？

我无法理解为什么在无类型lambda演算中允许以下beta减少:

(?x.x y) (u v) -> ((u v) y)

具体来说,我无法理解如何可以传递两个参数u和v到一个单一的参数x在?x.x一部分.允许以上不应该使用currying并有两个参数？像这样-

(?x.(?y.(x y))) (u v)

通过高阶函数可以在无类型lambda演算中编码各种类型.

Examples:
zero  = ?fx.      x
one   = ?fx.     fx
two   = ?fx.   f(fx)
three = ?fx. f(f(fx))
etc

true  = ?tf. t
false = ?tf. f

tuple = ?xyb. b x y
null  = ?p. p (?xy. false)

我想知道是否有任何研究已经嵌入其他不太常规的类型.如果有一些定理断言可以嵌入任何类型,那将是很棒的.也许有限制,例如只能嵌入类型*.

如果确实可以表示不太常规的类型,那么看一个例子就太棒了.我特别热衷于看看monad类型成员的样子.

min通常在无类型lambda演算上定义为(使用Caramel的语法):

sub a b   = (b pred a)
<=  a b   = (is_zero (sub b a))
min a b   = (<= a b a b)

这非常低效.Sub是二次的,因为它适用pred(这是线性的)b时间.有一个更有效的实现min:

min a b succ zero = (a a_succ (const zero) (b b_succ (const zero))))
    a_succ pred cont = (cont pred)
    b_succ pred cont = (succ (cont pred))

这将以延续传递方式切换两个数字,直到达到第一个零.现在,我正在尝试找到一个max效率高的min,具有以下属性:

1. a并且b在函数体上最多使用一次.

2. 它具有β正常形式(即,不使用定点组合器强烈正常化).

这样的max定义是否存在？

使用类似于Morte/CoC的语言,我试图证明这个简单的陈述there are lists of arbitrary lengths.为此,我写了以下类型:

? n:Nat ->
(ThereIs (List Nat)
  (Equal Nat 
    (List.length Nat l) 
    n)))

ThereIs是依赖对(Sigma).一切都是教会编码的.为证明这一点,我写了以下证据:

? n:Nat ->
(ThereIs.this (List Nat)
  (? l:(List Nat) -> (Equal Nat (List.length Nat l) n))
  (List.replicate Nat n Nat.Zero)
  (Equal.refl Nat n))

奇怪的是,我得到一个类型不匹配错误d(即Nat类型的自由变量)和? c:* -> ? b:(c -> c) -> ? a:c -> (d c b a).但是那个后期,当eta减少时,只是d!由于我没有准备好eta-reducer,我改为使用以下"无用识别"功能:

? n: Nat ->

? Nat:* ->
? Succ: (Nat -> Nat) ->
? …

假设我有两个以下类型的Haskell函数,并激活了ExplicitForAll,

f :: forall a. (a -> Int)
g :: forall a. (Int -> a)

在我看来,该类型g是同构Int -> (forall a. a)的,因为例如类型g(2)为forall a. a.

但是,类型f看起来并不是同构的(forall a. a) -> Int.f是一个多态函数,它知道在每个输入类型上计算什么a,在数学中我想它宁可是一系列函数; 但我认为它不能处理具有所有类型的单个参数.

是类型lambda演算的规则,类型量词分布在函数目标类型上,而不是函数源类型上吗？

该类型是否(forall a. a) -> Int存在于Haskell中,可能限制为类型类(forall a. SomeClass a => a) -> Int？它有用吗？

我试图在C++中不想要lambda演算和lambda表达式之间的联系.

首先,在无类型的lambda演算中,我们没有像booleans或int或whatevr这样的"基本值",所以一切都必须编码为函数,然后我们可以将任何术语应用于任何其他术语,但情况并非如此在C++中有一个类型系统.

此外,我已经看到lambda表达式要么在函数指针中转换(当它们没有捕获任何东西时),要么在函数中转换(仅用于包装函数的类).

所以我想知道,"lambda表达式"只是匿名函数的一个奇特名称,因此它类似于lambda演算(在某种意义上,lambda表达式中的术语可以看作是未命名的函数),还是有更多呢？

提前致谢.

虽然学习Haskell,我遇到了一个挑战,找到两个函数f和g,使得f g和f . g是等价的(总,所以像f = undefined或f = (.) f不计).给定的解决方案是f并且g都等于\x -> x . x(或join (.)).

(我注意到这不是Haskell特有的;它可以用纯粹的组合逻辑表示为"find fand gsuch that f g = B f g",然后给定的解决方案将转换为f = g = W B.)

我理解为什么给定的解决方案在扩展时会起作用,但我不明白如果你不知道它会怎么找到它.这是我能走多远:

• f g = f . g (给予)
• f g z = (f . g) z (双方的扩张)
• f g z = f (g z) (简化RHS)

而且我不知道如何从那里开始.在尝试寻找解决方案时,我会做什么？

我刚刚为即将到来的OCaml测试做了一些功课,我遇到了一些麻烦.

考虑由以下抽象语法定义的λ项的语言(其中x是变量):

t ::= x | t t | ?x. t  

写一个类型术语来表示λ术语.假设变量表示为字符串.

好的,男孩.

# type t = Var of string | App of (t*t) | Abs of string*t;;
type t = Var of string | App of (t * t) | Abs of (string * t)

术语t的自由变量fv(t)由归纳定义如下:

fv(x) = {x}  
fv(t t') = fv(t) ? fv(t')  
fv(?x. t) = fv(t) \ {x}

当然可以.

# let rec fv term = match term with
Var x -> [x]
  | App (t, t') …

文章更简单,更容易!声称即使没有"Pi"存在也可以对依赖类型系统进行编码 - 也就是说,你可以重复使用"Lam"构造函数.但是,如果在某些情况下对"Pi"和"Lam"的处理方式不同,那又怎么可能呢？

此外,可以删除"明星"吗？我认为你可以用"λx.x"(id)替换它的所有出现.