Let’s shift gears in our time machine. This time we’ll travel a lot closer, to the 1930s. The Great Depression was ravaging the New and the Old worlds. Almost every family from every social class was affected by the tremendous economic downturn. Very few sanctuaries remained where people were safe from the perils of poverty. Few people were fortunate enough to be in these sanctuaries, but they did exist. Our interest lies in mathematicians in Princeton University.
타임머신의 기어를 이동시켜 봅시다. 이번에는 좀더 가까운 1930 년대를 여행할 겁니다. 대공황은 신세계와 구세계를 모두 휩쓸고 지나갔습니다. 모든 사회의 거의 대부분의 가족이 이 경제적 하락에 심각한 영향을 받았습니다. 이 절대 부족의 위협속에서 안전한 곳은 거의 없었습니다. 이런 곳에 있을 만큼 운 좋은 사람들은 거의 없었지만 아예 없었던 것은 아닙니다. 이제 프린스톤 대학의 수학자들에게 눈을 돌려봅시다.
The new offices constructed in gothic style gave Princeton an aura of a safe haven. Logicians from all over the world were invited to Princeton to build out a new department. While most of America couldn’t find a piece of bread for dinner, high ceilings, walls covered with elaborately carved wood, daily discussions by a cup of tea, and walks in the forest were some of the conditions in Princeton.
고딕 스타일로 새로 지어진 프린스톤의 직무실들은 천국의 아우라를 뿜고 있었습니다. 새로운 학과를 만들기 위해 전 세계의 논리학자들이 프린스톤으로 초청되었습니다. 대다수의 미국인들이 저녁 끼니를 때울 빵을 구하지 못하는 상황이었지만 프린스톤의 모습은 그와 달랐습니다. 프린스턴의 천장은 높았으며, 벽은 섬세하게 조각된 나무로 덮여 있었고, 차를 마시며 일상 대화를 할 수 있었습니다. 산책할 수 있는 숲도 있었지요.
One mathematician living in such lavish lifestyle was a young man named Alonzo Church. Alonzo received a B.S. degree from Princeton and was persuaded to stay for graduate school. Alonzo felt the architecture was fancier than necessary. He rarely showed up to discuss mathematics with a cup of tea and he didn’t enjoy the walks in the woods. Alonzo was a loner: he was most productive when working on his own. Nevertheless Alonzo had regular contacts with other Princeton inhabitants. Among them were Alan Turing, John von Neumann, and Kurt Gödel.
그렇게 부족함 없이 생활할 수 있었던 수학자중 Alonzo Church 라는 젊은 남자가 있었습니다. Alonzo 는 프린스턴에서 학사 학위를 받았는데 학교는 대학원을 위해 계속 남아 있도록 그를 설득했습니다. Alonzo 는 건물들이 필요이상으로 사치스럽다고 생각했습니다. 수학자들의 티 타임에 거의 나타나지 않았습니다. 숲을 산책하는 것도 즐기지 않았습니다. Alonzo 는 혼자있는 것을 좋아했습니다. Alonzo 는 혼자 연구할 때 가장 생산적일 수 있었습니다. 그러지만 Alan Turing, John von Neumann, Kurt Gödel 과 같은 프린스톤 동료들과는 정기적인 만남을 가졌습니다.
The four men were interested in formal systems. They didn’t pay much heed to the physical world, they were interested in dealing with abstract mathematical puzzles instead. Their puzzles had something in common: the men were working on answering questions about computation. If we had machines that had infinite computational power, what problems would we be able to solve? Could we solve them automatically? Could some problems remain unsolved and why? Would various machines with different designs be equal in power?
이 네명의 수학자들은 formal system 에 관심을 가졌습니다. 그들은 물리적인 세계에 대해서는 별로 관심을 기울이지 않았습니다. 대신 추상적인 수학 퍼즐을 다루는데 관심이 있었습니다. 그들의 퍼즐에는 공통점이 있었는데 모두 계산(computation)에 대한 의문들을 푸는 것이었습니다. 만약 무한대의 연산 능력을 가진 기계가 생긴다면 어떤 문제를 풀 수 있을까? 이런 문제를 자동으로 풀 수 있을까? 어떤 문제들이 풀리지 않는다면 이유는 무엇일까? 서로 다른 디자인의 다양한 기계들은 같은 힘을 지닐까?
In cooperation with other men Alonzo Church developed a formal system called lambda calculus. The system was essentially a programming language for one of these imaginary machines. It was based on functions that took other functions as parameters and returned functions as results. The function was identified by a Greek letter lambda, hence the system’s name4. Using this formalism Alonzo was able to reason about many of the above questions and provide conclusive answers.
Alonzo 는 다른 수학자들과 협업하면서 lambda calculus 라고 불리는 formal system 을 개발하였습니다. Lambda calculus 는 사실 위에 언급한 가상 머신중 하나를 위한 프로그래밍 언어였습니다. Lambda calculus 는 펑션을 인자로 받아서 펑션을 결과로 리턴하는 펑션에 기반한 시스템입니다. 펑션은 그리스 문자 lambda 로 표시되었고 이 시스템 이름의 유래가 되었습니다. Alzono 는 이 형식적 기술법을 사용하여 계산에 관한 많은 의문들을 추론할 수 있었고 결정적인 답을 제공할 수 있었습니다.
Independently of Alonzo Church, Alan Turing was performing similar work. He developed a different formalism (now referred to as the Turing machine), and used it to independently come to similar conclusions as Alonzo. Later it was shown that Turing machines and lambda calculus were equivalent in power.
Alan Turing 은 Alonzo Church 와는 독립적으로 비슷한 작업을 하고 있었습니다. 그는 지금에 와서 Turing machine 이라고 불리는 기술법을 개발한 후 추론에 사용하여 Alonzo 와 비슷한 결론을 도출했습니다. 후에 Turing machines 과 lambda calculus 는 동등한 능력을 가졌음이 판명되었습니다.
This is where the story would stop, I’d wrap up the article, and you’d navigate to another page, if not for the beginning of World War II. The world was in flames. The U.S. Army and Navy used artillery more often than ever. In attempts to improve accuracy the Army employed a large group of mathematicians to continuously calculate differential equations required for solving ballistic firing tables. It was becoming obvious that the task was too great for being solved manually and various equipment was developed in order to overcome this problem. The first machine to solve ballistic tables was a Mark I built by IBM - it weighed five tons, had 750,000 parts and could do three operations per second.
2 차 세계 대전이 없었다면 여기가 이야기의 끝일 것이고, 저는 글을 마무리 지었을 것이고, 여러분은 다음 장으로 넘어갈 수 있었을 겁니다. 하지만, 세계는 화염에 휩싸였습니다. 미 육군과 해군은 과거 어느 때보다 대포를 많이 사용했습니다. 군대는 정확성을 높이기 위해 수학자들을 대규모로 고용하여 탄도 테이블 마련에 필요한 미분 방정식을 끊임없이 계산하게 했습니다. 이 일이 수작업으로 하기에는 너무나도 엄청난 일이라는 것이 명확해졌기 때문에 이 문제를 해결하기 위한 다양한 장비들이 개발되었습니다. 탄도 테이블을 계산한 최초의 기계는 IBM 이 만든 Mark I 이었습니다. 이 기계는 무게가 5 톤에, 750,000 개의 부품으로 구성되었고, 초당 3 개의 연산을 할 수 있었습니다.
The race, of course, wasn’t over. In 1949 an Electronic Discrete Variable Automatic Computer (EDVAC) was unveiled and had tremendous success. It was a first example of von Neumann’s architecture and was effectively a real world implementation of a Turing machine. For the time being Alonzo Church was out of luck.
경쟁은 이제 시작이었습니다. 1949 년에 소개된 EDVAC 은 매우 큰 성공을 거두었습니다. EDVAC 은 von Neumann 아키텍쳐를 사용한 최초의 기계였고 Turing machine 을 현실 세계에 구현한 것이었습니다. Alonzo Church 는 이 당시엔 운이 없었습니다.
In late 1950s an MIT professor John McCarthy (also a Princeton graduate) developed interest in Alonzo Church’s work. In 1958 he unveiled a List Processing language (Lisp). Lisp was an implementation of Alonzo’s lambda calculus that worked on von Neumann computers! Many computer scientists recognized the expressive power of Lisp. In 1973 a group of programmers at MIT’s Artificial Intelligence Lab developed hardware they called a Lisp machine - effectively a native hardware implementation of Alonzo’s lambda calculus!
1950 년대 말, 프린스턴을 졸업한 MIT 교수 John McCarthy 는 Alonzo Church 의 작업에 가졌던 관심을 발전시켜 나갔습니다. 그는 1958 년에 List Processing 언어 Lisp 를 발표했습니다. Lisp 는 von Neumann 컴퓨터 위에 Alzono 의 lamba calculus 를 구현한 것이었습니다. 많은 컴퓨터 과학자들이 Lisp 의 표현력이 가진 힘을 확인했습니다. 1973 년에는 MIT 인공지능 연구실의 프로그래머들이 Lisp machine 이라는 하드웨어를 개발했습니다. 이것은 lambda calculus 의 하드웨어적인 구현이었습니다.