标签: lambda-calculus

我记得在某处读过Hindley Milner是对system-f的限制.如果是这种情况,有人可以请我提供一些可以输入system-f但不能输入HM的条款.

我正在学习lambda演算,但我似乎无法理解数字0的编码.

" 函数接受函数和第二个值并将函数零次应用于参数 "为零？有没有其他方法来编码零？这里的任何人都可以帮我编码0吗？

我正在尝试stack使用定点组合器在lambda演算中定义数据结构.我试图定义两个操作,insertion以及removal元素,所以,push和pop,但是我能够定义的唯一一个,插入,不能正常工作.删除我无法弄清楚如何定义.

这是我对push操作的方法,我的定义是stack:

Stack definition:
STACK = \y.\x.(x y)
PUSH = \s.\e.(s e)

我的堆栈初始化为一个元素来指示底部; 我在0这里使用:

stack = STACK 0 = \y.\x.(x y) 0 = \x.(x 0)       // Initialization
stack = PUSH stack 1 = \s.\e.(s e) stack 1 =     // Insertion
    = \e.(stack e) 1 = stack 1 = \x.(x 0) 1 =
    = (1 0)

但是现在,当我尝试插入另一个元素时,它不起作用,因为我的初始结构已被解构.

如何修复STACK定义或PUSH定义,以及如何定义POP操作？我想我将不得不应用组合器,以允许递归,但我无法弄清楚如何做到这一点.

参考: …

我目前正在学习Haskell,还参加了一个关于大学函数式编程的理论讲座.

我知道这纯粹是理论/学术问题,但我感兴趣的是如何简单地用纯lambda演算来表达不同的简单函数(即没有定义任何常量).

我的一些讲义材料定义了布尔值,例如:

True =\xy.x
False =\xy.y

(\表示lambda符号)

如果它们被定义为这些选择器函数,则if条件可以很容易地定义为:

如果 =\xx

现在,我正在尝试为逻辑"和"函数提供一些简短形式.我的第一个猜测是:

和 =\XY {(如果 x)的[(如果 Y)真 假 ] 假 }

所以基本上这个lambda函数会接收2个参数uv,其中两个都必须输入类似True/False.如果我使用逻辑表的所有4种组合进行各种beta减少,我会收到正确的结果.

不过这个功能看起来有点难看,我正在考虑让它更优雅.这里有什么建议？

人们可以解释Haskell中的lambda演算:

data Expr = Var String | Lam String Expr | App Expr Expr

data Value a = V a | F (Value a -> Value a)

interpret :: [(String, Value a)] -> Expr -> Value a
interpret env (Var x) = case lookup x env of
  Nothing -> error "undefined variable"
  Just v -> v
interpret env (Lam x e) = F (\v -> interpret ((x, v):env) e)
interpret env (App e1 e2) = case interpret env e1 of …

据我所知,在Haskell等语言中,以及作为lambda演算的一部分,每个lambda表达式都有自己的作用域,所以如果我有嵌套的lambda表达式,例如:\x -> (\x -> x)那么第一个\x参数与第二个参数不同\x.

在Java中,如果执行此操作,则会出现编译错误,就像您x再次使用作为参数名称或lambda中的局部变量名称一样,如果它已在封闭范围内使用,例如作为方法参数.

有没有人知道为什么Java以这种方式实现了lambda表达式 - 为什么不让它们引入一个新的作用域级别并且表现得像一个匿名类呢？我假设是因为某些限制或优化,或者可能是因为lambdas必须被黑客入侵现有语言？

我正在用Greg Michaelson的"通过Lambda微积分进行功能编程简介"一书中学习lambda演算.

我仅使用该语言的一个子集在Clojure中实现示例.我只允许:

• 符号
• one-arg lambda函数
• 功能应用
• var定义为方便起见.

到目前为止,我有这些功能:

(def identity (fn [x] x))
(def self-application (fn [s] (s s)))

(def select-first (fn [first] (fn [second] first)))
(def select-second (fn [first] (fn [second] second)))
(def make-pair (fn [first] (fn [second] (fn [func] ((func first) second)))))    ;; def make-pair =  ?first.?second.?func.((func first) second)

(def cond make-pair)
(def True select-first)
(def False select-second)

(def zero identity)
(def succ (fn [n-1] (fn [s] ((s False) n-1))))
(def one (succ zero))
(def zero? (fn …

在Agda中,可以使用PHOAS方便地表示λ项:

data Term (V : Set) : Set where
  var : V ? Term V
  abs : (V ? Term V) ? Term V
  app : Term V ? Term V ? Term V

这种方法比Bruijn指数有几个好处,如"机械化语义的参数高阶抽象语法"中所述.据我所知,不能有一个eval : ? {V} -> Term V -> Term V函数,给定一个λ项,返回其正常形式 - 毕竟,Agda是完全的,而λ演算不是.但我想知道是否有可能eval为仿射λ项编写这样的函数; 即,绑定变量最多出现一次的那些.这种语言显然是完全的.

在之前的问题SystemT编译器和处理Haskell中的无限类型时,我询问了如何将SystemT Lambda微积分解析为SystemT组合器.我决定使用普通代数数据类型来编码SystemT Lambda演算和SystemT Combinator演算(基于注释:SystemT编译器和处理Haskell中的无限类型).

SystemTCombinator.hs:

module SystemTCombinator where

data THom = Id
          | Unit
          | Zero
          | Succ
          | Compose THom THom
          | Pair THom THom
          | Fst
          | Snd
          | Curry THom
          | Eval
          | Iter THom THom
          deriving (Show)

SystemTLambda.hs:

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE MultiParamTypeClasses     #-}
{-# LANGUAGE PartialTypeSignatures     #-}
{-# LANGUAGE TypeSynonymInstances      #-}

module SystemTLambda where

import           Control.Monad.Catch
import           Data.Either (fromRight)
import qualified SystemTCombinator    as SystemTC

type …

使用 De Bruijn 表示法，可以将 lambda 项定义为：

data BTerm = BVar Int | BLam BTerm | BApp BTerm BTerm

或者使用通常的符号， data Term = Var String | Lam String Term | App Term Term

这两种数据类型允许构造封闭项和包含自由变量的项。

是否可以定义仅允许构造封闭项的数据类型。即只有诸如：\xx、\x 之类的术语。xx, \x.\y. xy, \x.\y. y, \x.\y.\zz(xy)