JS와 Lambda Calculus 알아보기.(람다 대수)

원문 : https://glebec.github.io/lambda-talk/

Lambda as JS, or A Flock of Functions

앨런 튜링이 창안한 개념인 튜링 머신은 메모리, 명령어 등 기본적인 상태 기계를 위한 개념들을 정의한다.

처치-튜링 명제의 람다 대수는 순수함수 만으로 기계의 동작을 표현하며, 이는 함수형 프로그래밍의 기반이 된다.

그래서 상태를 어떻게 순수 함수들의 조합으로 표현하는가? 힌트는 currying에 있다.

 

IDENTITY(I)

흔하게 보는 항등 함수다.

λ기호는 함수의 시작(람다의 추상화 시작)을 의미한다.

.의 왼쪽은 파라미터를 의미한다.

오른쪽은 return expression을 의미한다.

header('I := λx.x') // :=는 오른쪽으로 정의됨을 의미함.
const I = x => x


const tweet = Symbol('tweet')
const chirp = Symbol('chirp')

// 실행 결과는 다음과 같다.
demo('I tweet = tweet', I(tweet) === tweet)
demo('I chirp = chirp', I(chirp) === chirp)

람다 대수에서 유효한 argument는 람다 추상화(함수)를 포함한다.

즉 함수는 1급이다.

(1급 함수 복습 : 함수 인자 가능. 함수 리턴 가능, 변수에 함수 할당 가능)

함수는 동사(계산을 수행할 수 있음) 및 명사(계산의 주어 또는 대상이 될 수 있음)의 역할 둘 다 가능합니다.

// I I 람다 대수에서 나란히 두는 것은, 오른쪽을 왼쪽에 인자로 적용한다는 뜻이다.
// = (λx.x)(λx.x)
// = λx.x

demo('I I = I', I(I) === I)

SELF-APPLICATION

위에서 II는 I였다.

즉 I를 여러번 자신에게 적용해도 I다.

하스켈 커리는 새를 매우 좋아했다고 한다, 논리학자 Raymond Smullyan은 커리를 기리며 많은 조합 논리(함수)에 새의 이름을 붙였다.

이번에 볼 함수는 MockingBird(흉내지빠귀)다. ω로도 표기한다.

이 함수는 함수를 인자로 받아 인바로 받은 함수에 자기 자신을 적용한다.

header('Mockingbird := M := ω := λf.ff')

const ω = fn => fn(fn)
const M = ω
const Mockingbird = M

// M I = (λf.ff)(λx.x) = (λx.x)(λx.x) = I I = λx.x = I
demo('M I = I I = I', M(I) === I(I) && I(I) === I)

M에 M을 적용하면? Ω (big Omega) Combinator로, 끝나지 않는다. 이는 정지 문제를 상기하게 한다.

// M M = (λf.ff)(λf.ff) = (λf.ff)(λf.ff) = (λf.ff)(λf.ff) = (λf.ff)(λf.ff) ...
try {
  M(M)
} catch (err) {
  demo('M M = M M = M M = ' + err.message, true)
}

CHURCH ENCODINGS: BOOLEANS

프로그래밍의 진정한 힘은 논리를 다룰 때 (비즈니스 로직) 나타난다.

함수만으로 Boolean을 표현 가능할까?

람다 대수의 bool은 두 개의 인수 중 하나를 선택하는 함수다.

λabc.a는  λa.λb.λc.a, or λa.(λb.(λc.a)))와 같다. 즉 모든 함수가 커링이 적용된다.

header('T := λxy.x = λx(λy.x)')  
// (1. ()안의 x는 인자로 받은 실제 x값이 되며. 2. y는 아무 역할을 못하기에 x를 리턴함)
// x => y => x 
const T = thn => els => thn

header('F := λxy.y')
const F = thn => els => els
 
demo('T tweet chirp = tweet', T(tweet)(chirp) === tweet)
demo('F tweet chirp = chirp', F(tweet)(chirp) === chirp)

 위 내용이 이해가 잘 안되면 하스켈의 in operator의 역할을 생각하면 된다 (expression안의 identifier를 실제 값으로 치환한다.)

FLIPPING ARGUMENTS

Cardinal Combinator는 인자의 순서를 뒤집는다.

즉  T를 뒤집어 F를 얻을 수 있다.

header('Cardinal := C := flip := λfab.fba')
const flip = func => a => b => func(b)(a)
const C = flip
const Cardinal = C
// With the Cardinal, we can derive F from the flip of T:
header('F = C T')

demo('flip T tweet chirp = chirp', flip(T)(tweet)(chirp) === chirp)

 

NEGATION(부정)

람다 대수의 bool은 두 개의 인수 중 하나를 선택하는 함수였다.

또한 Cardinal은 인자의 순서를 뒤집는 함수였다.

각각을 이용하면,  부정을 도출할 수 있다.

header('NOT := λb.bFT')
const NOT = chooseOne => chooseOne(F)(T)




demo('NOT T = F', NOT(T) === F)
demo('NOT F = T', NOT(F) === T)
// NOT T = (λb.bFT) T = TFT = (λxy.x) F T = F
demo('CF = T', C(F)(tweet)(chirp) === tweet)
// NOT F = (λb.bFT) F = FFT = (λxy.y) F T = T
demo('CT = F', C(T)(tweet)(chirp) === chirp)

 CONJUNCTION AND DISJUNCTION (And or Not)

두개의 파라미터 인자를 받아 적절한 불리언 인자인지 확인하다.

(커링일 뿐임을 상기하자.)

header('AND := λpq.pqF') // λpq.pqp 
const AND = p => q => p(q)(F)

demo('AND F F = F', AND(F)(F) === F)
demo('AND T F = F', AND(T)(F) === F)
demo('AND F T = F', AND(F)(T) === F)
demo('AND T T = T', AND(T)(T) === T)

OR은 다음과 같다.

(True는 첫번째 인자를 리턴한다.

False는 두번째 인자를 리턴한다.)

 

header('OR := λpq.pTq') // λpq.ppq
const OR = p => q => p(T)(q)
const OR = p => q => p(p)(q)
demo('OR F F = F', OR(F)(F) === F)
demo('OR T F = T', OR(T)(F) === T)
demo('OR F T = T', OR(F)(T) === T)
demo('OR T T = T', OR(T)(T) === T)

// λpq.ppq에서 pp는 M과 비슷함
// 즉 M으로 모델링할 수 있음
// λp.(λq.ppq) => ω(p)(q)
header('Mockingbird := M := ω := λf.ff')
demo('M F F = F', M(F)(F) === F)
demo('M T F = T', M(T)(F) === T)
demo('M F T = T', M(F)(T) === T)
demo('M T T = T', M(T)(T) === T)

DEMO: DE MORGAN’S LAWS

아직 boolan equality는 배우지 않았음.

header('De Morgan: not (and P Q) = or (not P) (not Q)')

function deMorgansLawDemo (p, q) { return NOT(AND(p)(q)) === OR(NOT(p))(NOT(q)) }

demo('NOT (AND F F) = OR (NOT F) (NOT F)', deMorgansLawDemo(F, F))
demo('NOT (AND T F) = OR (NOT T) (NOT F)', deMorgansLawDemo(T, F))
demo('NOT (AND F T) = OR (NOT F) (NOT T)', deMorgansLawDemo(F, T))
demo('NOT (AND T T) = OR (NOT T) (NOT T)', deMorgansLawDemo(T, T))

BOOLEAN EQUALITY

대충 and가 필요할 것이라고는 짐작이 된다.

header('T := λxy.x = λx(λy.x)')  

const T = thn => els => thn

header('F := λxy.y')
const F = thn => els => els

header('AND := λpq.pqF') // λpq.pqp 
const AND = p => q => p(q)(F)

header('BEQ := λpq.p (qTF) (qFT)')
const BEQ = p => q => p( q(T)(F) )( q(F)(T) )

demo('BEQ F F = T', BEQ( BEQ(F)(F) )(T))
demo('BEQ F T = F', BEQ( BEQ(F)(T) )(F))
demo('BEQ T F = F', BEQ( BEQ(T)(F) )(F))
demo('BEQ T T = T', BEQ( BEQ(T)(T) )(T))

 

이해 안될만한 내용.

1. 왜 boolean인데 true, false가 등장 안하는가?

> 해당 부분은 타입 이론이 나와야 적용됨. 람다 대수는 타입에 대해 다루지 않음

> 나중에 나올 numeric은 함수의 중첩으로 정의됨.

> 지금까지 등장한 모든 함수, 데이터는 하나의 심볼 혹은 0,1과 같은 개념으로 생각할 수 있음

2. 왜 저 람다 대수가 AND, OR이 되는지?

> 진리표와 같은 느낌으로 접근해야 할 듯?

 

 

추가 예정 내용 : 대수 타입