수학 개념 지도
인물

요아힘 람베크(Joachim Lambek)

낱말에 타입⁠(type)⁠을 주어 문장의 문법을 계산하는 범주 문법(람베크 계산⁠, Lambek calculus⁠)을 만들고, 논리의 증명과 타입 붙은 람다 계산⁠(lambda calculus)⁠과 데카르트 닫힌 범주⁠(cartesian closed category)⁠가 서로 대응한다는 것을 보인 캐나다의 수학자.

n⋅(n\s)  →  sn \cdot (n \backslash s) \;\to\; s

요아힘 람베크는 1922년 독일 라이프치히에서 태어났습니다. 1938년 나치 독일의 박해를 피해 유대계 아이들을 영국으로 보낸 킨더트랜스포트로 영국에 건너갔지만, 1940년 전쟁이 번지자 적국 출신이라는 이유로 억류되어 캐나다 뉴브런즈윅의 수용소로 보내졌습니다. 수용소 안에서 대학 입학 시험을 치렀고, 1942년 풀려나 몬트리올에 자리 잡았습니다. 이후 평생을 맥길 대학에서 보냈고, 1950년 그곳의 첫 수학 박사가 되었습니다. 학위 논문의 한 주제는 반군⁠(semigroup)⁠, 곧 결합 법칙만 성립하는 곱셈이 있는 대수 구조를 군 속에 넣을 수 있는 조건이었습니다.

굵은 막대가 이 사람의 생애이고, 흰검은 점은 페이지 끝 연표에 적은 일들입니다. 가는 막대는 같은 시대를 산 이 위키의 인물들입니다. 나이를 끌어 보세요.

나이 세 ·

대수학자인 그의 이름이 먼저 알려진 곳은 뜻밖에 언어학이었습니다. 1958년 논문 「문장 구조의 수학」에서 그는 낱말마다 타입을 주었습니다. 이름은 nn, 문장은 ss이고, 자동사 "잔다"는 "왼쪽에 이름이 오면 문장이 된다"는 뜻의 n\sn \backslash s, 타동사 "좋아한다"는 "왼쪽과 오른쪽에 이름이 오면 문장이 된다"는 뜻의 (n\s)/n(n \backslash s) / n입니다. 위의 식처럼 이웃한 타입을 분수의 약분처럼 줄여 ss가 남으면 그 낱말의 줄은 문장입니다. 이것이 범주 문법⁠(categorial grammar)⁠의 논리, 곧 람베크 계산입니다. 규칙은 논리의 '이면'을 쓰는 추론과 같은 모양이되, 낱말의 순서가 중요하니 가정의 자리를 바꾸는 규칙이 없습니다. 오늘날의 말로는 교환 법칙이 없는 선형 논리⁠(linear logic)⁠의 한 조각입니다. 같은 무렵 촘스키가 내놓은 문맥 자유 문법⁠(context-free grammar)⁠과 이 문법이 같은 언어들을 기술한다는 것은 1993년 마테이 펜타가 증명했습니다.

1968년부터 1972년까지 그는 「연역 체계와 범주⁠(category)⁠」라는 제목의 논문 세 편에서 이 생각을 범주론⁠(category theory)⁠으로 옮겼습니다. 논리의 증명, 커리의 조합 논리⁠(combinatory logic)⁠와 타입 붙은 람다 계산의 프로그램, 그리고 데카르트 닫힌 범주의 화살표가 서로 정확히 대응한다는 것입니다. 곱은 '그리고', 지수 대상⁠(exponential object)⁠은 '이면', 화살표는 증명입니다. 필립 스콧과 함께 쓴 1986년 책 『고차 범주 논리 입문』은 이 대응을 정리하고, 고차 논리와 토포스⁠(topos)⁠가 서로의 모형이 된다는 것까지 다루었습니다. 그래서 이 대응을 흔히 커리–하워드–람베크 대응이라 부릅니다.

그는 말년에 다시 언어로 돌아왔습니다. 1999년 무렵부터 타입의 계산을 더 단순한 대수 구조(프리그룹)로 바꾸어 여러 언어의 문법을 기술했고, 2008년 『낱말에서 문장으로』로 정리했습니다. 이 대수는 뒤에 문장의 뜻을 벡터⁠(vector)⁠로 계산하려는 연구에서 문법의 뼈대로 쓰였습니다. 1992년 은퇴한 뒤에도 맥길에서 연구를 이어 갔고, 2014년 몬트리올에서 아흔한 살로 세상을 떠났습니다.

이어지는 곳. 증명과 프로그램과 화살표의 대응은 커리–하워드 대응⁠(Curry–Howard correspondence)⁠과 데카르트 닫힌 범주에서, 그 바탕인 범주론과 수반은 각각의 페이지에서 볼 수 있습니다. 문법을 규칙으로 보는 다른 전통은 촘스키 위계⁠(Chomsky hierarchy)⁠와 문맥 자유 문법에 있습니다.

관계.

가운데가 이 사람, 둘레가 이어진 인물들입니다. 선의 색은 관계의 종류(초록 스승·제자, 파랑 함께 연구, 보라 편지, 빨강 논쟁, 주황 영향)이고, 다른 인물의 페이지에 적힌 관계도 함께 모았습니다.

  • 영향을 받음 해스켈 커리 — 1968–1972년의 연작에서 커리의 조합 논리와 함의 논리, 그리고 데카르트 닫힌 범주가 서로 대응한다는 것을 보여, 커리–하워드 대응에 범주의 얼굴을 더했습니다.
  • 영향을 받음 윌리엄 로베어 — 로베어가 시작한 흐름, 곧 범주론으로 논리를 다시 쓰는 흐름 속에서 일했고, 스콧과 쓴 1986년 책은 로베어와 티어니의 토포스를 고차 논리의 모형으로 다루었습니다.

연표.

  • 1922년 독일 라이프치히에서 태어나다
  • 1938년 유대계 아이들을 구한 킨더트랜스포트로 영국에 건너가다
  • 1940년 적국인으로 억류되어 캐나다 뉴브런즈윅의 수용소로 보내지다
  • 1942년 풀려나 몬트리올에 자리 잡다
  • 1945년 맥길 대학 수학과를 졸업하다
  • 1950년 맥길 대학 첫 수학 박사 학위를 받다
  • 1958년 「문장 구조의 수학」에서 람베크 계산을 내놓다
  • 1963년 맥길 대학 정교수가 되다
  • 1968년 「연역 체계와 범주」 연작을 시작하다
  • 1986년 필립 스콧과 『고차 범주 논리 입문』을 내다
  • 2008년 『낱말에서 문장으로』를 내다
  • 2014년 몬트리올에서 세상을 떠나다
관련 인물윌리엄 하워드

이 인물이 나오는 긴 글

타입 이론과 범주론 증명은 프로그램이다 러셀의 역설을 막으려던 '타입'이 프로그램의 실수를 막는 장치가 되었다. 명제를 타입으로, 증명을 프로그램으로 읽으면 둘이 규칙 하나하나까지 맞아떨어진다. 오늘날 수학자들은 그 사실로 컴퓨터에게 증명을 검사받는다. 범주론 화살표만으로 본 수학 최대공약수와 교집합과 '그리고'는 같은 것이고, 화살표를 뒤집으면 최소공배수와 합집합과 '또는'이 된다. 무엇으로 만들었는지 묻지 않고 어떻게 이어지는지만 보는 언어로, '자연스럽다'는 말의 뜻, 관계만으로 대상을 알아보는 요네다의 생각, 함자로 본 연쇄법칙, 어디에나 있는 수반까지 사이트의 여러 분야를 가로지른다.

이 인물을 언급하는 페이지

이 페이지가 가리키는 개념