연합우주란 무엇일까?

X(구 Twitter)나 Instagram 같은 중앙화된 소셜 미디어에 지치셨나요? 데이터 프라이버시, 알고리즘 추천, 그리고 끊임없는 광고가 걱정되시나요? 여기 대안이 있습니다. 바로 연합우주(fediverse)입니다.

페디버스(fediverse)는 “federated”(연합된)와 “universe”(우주)를 합친 말로, 한국어권에서는 주로 “연합우주”라고 불립니다. 연합우주는 하나의 거대한 플랫폼이 아닌, 서로 대화할 수 있는 독립적인 서버(인스턴스)들의 네트워크입니다.

이게 어떻게 가능할까요? 바로 ActivityPub이라는 프로토콜 덕분입니다. 이 프로토콜은 서로 다른 소셜 미디어 플랫폼이 정보를 교환할 수 있게 해주는 공통 언어 같은 것입니다.

연합우주는 어떻게 작동하나요?

연합우주를 이해하는 가장 쉬운 방법은 이메일 시스템과 비교하는 것입니다.

Gmail 사용자가 네이버 메일 사용자에게 이메일을 보낼 수 있는 것처럼, Mastodon 사용자는 Misskey나 PeerTube 사용자와 소통할 수 있습니다. (Mastodon, Misskey, PeerTube가 무엇인지는 아래에서 설명하겠습니다. Gmail과 네이버처럼 서로 다른 서비스라고 보시면 됩니다.) 이것이 가능한 이유는 이 서비스들이 모두 같은 언어인 ActivityPub 프로토콜로 대화하기 때문입니다.

연합우주에서 사용자 ID는 @사용자명@인스턴스.도메인 형식으로 되어 있습니다. 이메일 주소와 매우 비슷하죠? 예를 들면:

• @honggildong@mastodon.social: mastodon.social 인스턴스 사용자
• @kimcheolsu@pixelfed.social: pixelfed.social 인스턴스 사용자
• @leeyeonghui@misskey.io: misskey.io 인스턴스 사용자

연합우주의 다양한 플랫폼 둘러보기

연합우주는 마치 여러 행성으로 이루어진 태양계 같습니다. 각 행성(플랫폼)은 고유한 특성을 가지고 있지만, 모두 같은 우주(연합우주)에 속해 있죠. 아래 표에서 주요 플랫폼들을 살펴봅시다:

플랫폼	설명	주요 인스턴스	특징
Mastodon	X(구 Twitter)와 유사한 마이크로블로깅 플랫폼	• mastodon.social (공식 인스턴스) • 우리.인생 (한국 중심)	500자 제한의 짧은 게시물, 해시태그, 컨텐츠 경고 기능
Misskey	일본에서 개발된 고도로 커스터마이징 가능한 마이크로블로깅 플랫폼	• misskey.io (가장 인기 있는 일본 인스턴스) • 스텔라 (한국 중심)	리액션, 게임, 채팅 등 다양한 기능, 높은 커스터마이징 가능성
Pixelfed	Instagram과 유사한 이미지 공유 플랫폼	• pixelfed.social (공식 인스턴스) • 추억:사진 (한국 중심)	스토리, 필터, 발견 기능
PeerTube	YouTube와 유사한 비디오 호스팅 플랫폼	• PeerTube.TV	P2P 기술로 비디오 스트리밍, 채널, 재생목록
WriteFreely	미니멀한 블로그 플랫폼	• write.as	Markdown 지원, 심플한 디자인
Lemmy	Reddit과 유사한 링크 애그리게이터 및 토론 플랫폼	• lemmy.ml • YuruLemmy (한국 중심)	커뮤니티(서브레딧과 유사), 투표, 토론

플랫폼 vs 인스턴스: 무슨 차이가 있을까?

연합우주를 이해할 때 흔히 혼동되는 개념이 있습니다. 바로 플랫폼(소프트웨어)과 인스턴스(서버)의 차이인데요.

플랫폼은 Mastodon, Misskey, Pixelfed와 같은 소프트웨어 자체를 의미합니다. 이들은 오픈 소스 소프트웨어로, 누구나 다운로드받아 설치할 수 있습니다.

인스턴스는 그 소프트웨어를 실행하는 개별 서버를 말합니다. mastodon.social과 우리.인생은 모두 Mastodon 플랫폼을 실행하는 별도의 인스턴스입니다.

Meta의 Threads 같은 일부 서비스는 플랫폼과 인스턴스가 동일합니다. 하지만 대부분의 연합우주 서비스는 여러 인스턴스로 구성되어 있습니다.

연합우주의 매력 포인트

연합우주가 갖는 몇 가지 매력적인 특징이 있습니다:

1. 탈중앙화: 특정 기업이 모든 데이터와 규칙을 통제하지 않습니다. 각 인스턴스는 자체 규칙을 가질 수 있습니다.
2. 데이터 주권: 자신의 데이터에 대한 더 많은 통제권을 가질 수 있습니다.
3. 검열 저항성: 한 인스턴스가 차단되더라도 다른 인스턴스로 쉽게 이동할 수 있습니다.
4. 커뮤니티 중심: 각 인스턴스는 특정 관심사나 지역 커뮤니티를 중심으로 형성됩니다.
5. 다양성: 다양한 플랫폼과 인스턴스가 존재하여 선택의 폭이 넓습니다.

연합우주 시작하기

연합우주에 참여하는 것은 생각보다 쉽습니다:

1. 자신의 관심사나 지역과 관련된 인스턴스를 선택합니다.
2. 해당 인스턴스에 계정을 만듭니다.
3. 다른 인스턴스의 사용자들을 팔로우하고 소통을 시작합니다!

한국 사용자라면 Mastodon 인스턴스인 우리.인생, Misskey 인스턴스인 스텔라 같은 한국어 중심 인스턴스를 추천합니다. 한국어 환경을 지원하고 한국 사용자들이 활발하게 활동하고 있어 시작하기 좋습니다.

아니면 이 글이 올라온 Hackers' Pub도 괜찮습니다. 소프트웨어 엔지니어들을 위한 소셜 미디어랍니다. 아직 개발중이라 공개적으로 가입을 받고 있지는 않습니다만, 홍민희에게 연락 주시면 계정을 생성해 드릴 수 있습니다.

ActivityPub: 연합우주의 심장

이제 개발자 관점에서 ActivityPub이 어떻게 작동하는지 자세히 살펴보겠습니다.

ActivityPub은 W3C에서 권장하는 표준 프로토콜로, 분산 소셜 네트워킹의 기반이 됩니다. ActivityStreams 2.0 데이터 형식을 기반으로 하며, 서로 다른 서버 간에 정보를 교환하는 방법을 정의합니다.

ActivityPub의 핵심 개념

ActivityPub은 몇 가지 핵심 개념으로 구성됩니다:

1. 액터(actor): 사용자, 그룹 등 행동을 수행할 수 있는 주체입니다. 각 액터는 고유한 URL을 가지며, 수신함(inbox)과 발신함(outbox)을 가집니다.
2. 액티비티(activity): 액터가 수행하는 행동으로, 게시물 작성, 댓글 좋아요, 다른 사용자 팔로우 등이 있습니다.
3. 객체(object): 텍스트 게시물, 이미지, 비디오와 같이 생성되고 공유되는 콘텐츠입니다.

실제 작동 방식

홍길동(@honggildong@mastodon.social)이 게시물을 작성하고, 이영희(@leeyeonghui@misskey.io)가 이에 반응하는 과정을 살펴봅시다:

1. 게시물 작성: 홍길동이 Mastodon에서 게시물을 작성합니다. Mastodon 서버는 이 게시물을 ActivityStreams 2.0 형식의 Create(Note) 액티비티로 변환합니다. 이 액티비티는 홍길동의 팔로워(이영희 포함)에게 전달됩니다.

2. 게시물 수신: 이영희의 Misskey 서버는 이 액티비티를 받고 처리하여 이영희의 타임라인에 홍길동의 게시물을 표시합니다.

3. 상호작용: 이영희가 게시물에 좋아요를 누르면, Misskey 서버는 Like(Note) 액티비티를 생성하여 홍길동의 Mastodon 서버로 보냅니다. 홍길동은 이영희가 자신의 게시물을 좋아했다는 알림을 받게 됩니다.

마치 다른 언어를 사용하는 사람들이 통역사를 통해 대화하는 것과 비슷하죠? ActivityPub이 바로 그 통역사 역할을 합니다.

ActivityPub의 실제 메시지 들여다보기

개발자로서 실제 ActivityPub 메시지가 어떻게 생겼는지 궁금하실 텐데요. 몇 가지 예시를 살펴봅시다:

1. 사용자 프로필(액터) 정보

{
  "@context": [
    "https://www.w3.org/ns/activitystreams",
    "https://w3id.org/security/v1"
  ],
  "id": "https://mastodon.social/users/honggildong",
  "type": "Person",
  "preferredUsername": "honggildong",
  "name": "홍길동",
  "summary": "연합우주의 개척자",
  "inbox": "https://mastodon.social/users/honggildong/inbox",
  "outbox": "https://mastodon.social/users/honggildong/outbox",
  "followers": "https://mastodon.social/users/honggildong/followers",
  "following": "https://mastodon.social/users/honggildong/following",
  "publicKey": {
    "id": "https://mastodon.social/users/honggildong#main-key",
    "owner": "https://mastodon.social/users/honggildong",
    "publicKeyPem": "-----BEGIN PUBLIC KEY-----\n...\n-----END PUBLIC KEY-----"
  },
  "icon": {
    "type": "Image",
    "mediaType": "image/jpeg",
    "url": "https://mastodon.social/system/accounts/avatars/000/000/001/original/avatar.jpg"
  }
}

이 JSON 데이터는 홍길동의 프로필 정보를 담고 있습니다. 사용자 이름, 소개, 프로필 사진 URL, 그리고 중요한 inbox와 outbox URL이 포함되어 있죠.

2. 게시물 작성 액티비티

{
  "@context": "https://www.w3.org/ns/activitystreams",
  "id": "https://mastodon.social/users/honggildong/statuses/123456/activity",
  "type": "Create",
  "actor": "https://mastodon.social/users/honggildong",
  "published": "2025-02-21T14:30:00Z",
  "to": [
    "https://www.w3.org/ns/activitystreams#Public"
  ],
  "cc": [
    "https://mastodon.social/users/honggildong/followers"
  ],
  "object": {
    "id": "https://mastodon.social/users/honggildong/statuses/123456",
    "type": "Note",
    "content": "<p>연합우주에 오신 것을 환영합니다! #fediverse #연합우주</p>",
    "published": "2025-02-21T14:30:00Z",
    "attributedTo": "https://mastodon.social/users/honggildong",
    "to": [
      "https://www.w3.org/ns/activitystreams#Public"
    ],
    "cc": [
      "https://mastodon.social/users/honggildong/followers"
    ],
    "tag": [
      {
        "type": "Hashtag",
        "href": "https://mastodon.social/tags/fediverse",
        "name": "#fediverse"
      },
      {
        "type": "Hashtag",
        "href": "https://mastodon.social/tags/연합우주",
        "name": "#연합우주"
      }
    ]
  }
}

이것은 홍길동이 게시물을 작성했을 때 생성되는 Create(Note) 액티비티입니다. 게시물 내용, 해시태그, 공개 범위 등이 포함되어 있습니다.

3. 팔로우 액티비티

{
  "@context": "https://www.w3.org/ns/activitystreams",
  "id": "https://misskey.io/users/leeyeonghui/follow/1234",
  "type": "Follow",
  "actor": "https://misskey.io/users/leeyeonghui",
  "object": "https://mastodon.social/users/honggildong"
}

이영희가 홍길동을 팔로우할 때 생성되는 Follow 액티비티입니다. 단순하죠?

ActivityPub 서버 구현하기: 개발자를 위한 팁

직접 ActivityPub 서버를 구현하고 싶다면 다음 단계를 따라야 합니다:

1. 액터 구현: 사용자 프로필 정보를 ActivityStreams 형식으로 제공합니다.
2. 수신함과 발신함 설정: HTTP 엔드포인트를 만들어 액티비티를 받고 전송합니다.
3. 서명 및 인증: HTTP Signatures를 사용하여 요청을 서명하고 검증합니다.
4. 액티비티 처리: 다양한 액티비티 유형(Create, Follow, Like 등)을 처리하는 로직을 구현합니다.
5. 데이터 저장: 사용자, 게시물, 액티비티 등의 정보를 데이터베이스에 저장합니다.
6. 연합 정책 구현: 어떤 인스턴스와 연합할지, 어떤 컨텐츠를 허용할지 등을 설정합니다.

개발을 시작하기 전에 Mastodon, Misskey 같은 기존 구현체의 코드를 살펴보는 것이 도움이 됩니다. 처음부터 모든 것을 구현하는 것보다 Fedify 같은 프레임워크를 활용하는 것도 좋은 방법입니다.

WebFinger: 사용자를 찾는 방법

연합우주에서 @leeyeonghui@misskey.io 같은 사용자 ID를 어떻게 실제 ActivityPub 액터 URL로 변환할까요? 그 비밀은 WebFinger 프로토콜에 있습니다:

GET https://misskey.io/.well-known/webfinger?resource=acct:leeyeonghui@misskey.io

이 요청을 보내면 서버는 다음과 같은 응답을 반환합니다:

{
  "subject": "acct:leeyeonghui@misskey.io",
  "links": [
    {
      "rel": "self",
      "type": "application/activity+json",
      "href": "https://misskey.io/users/leeyeonghui"
    }
  ]
}

이제 https://misskey.io/users/leeyeonghui URL을 통해 사용자의 전체 프로필 정보를 얻을 수 있습니다. 마치 전화번호부에서 이름으로 전화번호를 찾는 것과 비슷하죠!

연합우주의 도전 과제와 미래

연합우주는 계속 성장하고 있지만, 몇 가지 도전 과제도 있습니다:

1. 확장성: 수많은 서버 간의 통신을 효율적으로 처리하는 것은 쉽지 않습니다.
2. 모더레이션: 각 인스턴스가 자체 규칙을 가지므로 콘텐츠 조정에 일관성이 부족할 수 있습니다.
3. 발견성: 중앙화된 플랫폼에 비해 새로운 사용자나 콘텐츠를 찾기 어려울 수 있습니다.
4. 사용자 경험: 일부 플랫폼은 아직 UI/UX 측면에서 개선이 필요합니다.

그러나 Threads와 같은 주요 서비스들이 ActivityPub을 채택하기 시작하면서, 연합우주의 미래는 밝아 보입니다. 개발자로서, 이런 성장하는 생태계에 참여할 수 있는 기회가 많이 있습니다.

마무리

연합우주와 ActivityPub은 중앙화된 소셜 미디어의 대안으로서 점점 더 주목받고 있습니다. 사용자에게 더 많은 통제권을 부여하고, 다양하고 풍부한 온라인 경험을 제공하는 연합우주의 세계는 계속해서 확장되고 있습니다.

개발자로서, 여러분은 이 새로운 탈중앙화된 웹의 생태계에 기여할 수 있습니다. 기존 애플리케이션에 ActivityPub 지원을 추가하거나, 완전히 새로운 서비스를 만들거나, 현재의 도전 과제를 해결하는 솔루션을 개발할 수 있습니다.

한국 개발자들의 참여가 늘어나면 한국 사용자들을 위한 더 다양하고 풍부한 서비스가 생길 것이고, 이는 더 건강하고 다양한 인터넷 문화를 만드는 데 기여할 것입니다.

그럼, 연합우주로의 여행을 시작해 보시는 건 어떨까요?

1.

함수형에선, 스트림 [1,2,3]에
(+1)을 map해서 [2,3,4]를 만들고,
(+2)를 map해서 [3,4,5]를 만드는 작업을,
(+2) ∘ (+1)를 [1,2,3]에 map하는 걸로 표현할 수 있어야 한다.

(+1), (+2), ((+2) ∘ (+1)) 함수들은 모두 Int -> Int 함수를 원하는 곳에 넣어 줄 수 있는 함수들이다.

위와 같이, 완벽하게 정보를 유지하진 않지만, 같은 "류"의 작업을 두 번 하는 것을, 한 번 작업하는 것으로 표현할 수 있는 경우도 있다. 예를 들어, 첫 번째 작업으로, "hello"를 로그로 남기고, 두 번째 작업으로, " world"를 로그로 남기는데, 이를 한 번의 작업으로, "hello world"를 로그로 남기는 작업으로 표현할 수 있다. 여기는 로그를 남기는 횟수 정보는 필요 없고, 최종 로그만 필요하다는 인위적 정보 선택이 들어가 있다. 이 인위적 선택(여기선 로그 문자열을 합치는 것)을 수긍해야만 가능하다.

로그를 남기는 작업을 m이라 부를 때, m a를 받는 곳에 m (m a)를 넘길 방법이 생긴다는 뜻이다. 달리 말하면, m (m a)로 표현되는 작업을 인위적인 절차를 거쳐 m a로 만들어도, 내가 필요한 정보는 사라지지 않는다는 뜻이다.

2.

무언가가 하나인데, 유심히 보면 하나가 아닌 경우, 이게 바로 모노이드다. mono는 하나를 뜻하고, ~oid는 "척"하는 걸 말한다. (예. 인간인 척 하는 휴머노이드) 하나인척 하는 게 모노이드다. 수학 책 앞 부분에서 이항 연산, 결합 법칙, 항등원이 있으면 모노이드라는 설명을 하는데, 그래서 모노이드가 뭐에 쓰는 물건인지는 한참 공부해야 알 게 된다.

(아래는 혼자만의 생각입니다.)
모노이드를 바라 보는 눈 중 하나로, "모든 대상을 이항 연산으로 표현"을 들 수 있다.

0을 포함한 자연수들 0,1,2,3,... 들은, + 이항 연산과, 이 연산의 항등원 0이 있으면, 모두 ○ + ○ 한 가지 모양으로 표현할 수 있게 된다.
0 -> 0+0
1 -> 0+1
2 -> 0+(1+1) = 1+1
...
모노이드 구조이기에, 어딘가에서 ○ + ○ 모양을 원한다면, 0,1,2,3,...을 모두 넣어 줄 수 있다.

3.

"어딘가에서 m a를 원한다면, m a, m (m a), m (m (m a)), ...를 모두 넣어 줄 수 있다."를 위와 비교하며 보자.

위에서 얘기한 인위적 선택 작업을 join으로 표현하면,
m (m a) --join--> m a
m (m (m a)) --join--> m (m a) --join--> m a
...
m 반복 작업을 모두 ○ --join--> ○ 모양으로 표현할 수 있을 것만 같다. 그런데, 딱 하나는 표현하지 못한다. join은 m이 두 개 있는 걸, 하나로 만드는 작업이라, m하나를 ○ --join--> ○로 표현하지 못한다. m을 join이 들어간 모양으로 표현하려면, 자연수, + 에서 처럼 0에 대응하는 것이 필요하다. m하나를, m 두 개로 만들되, 최종 결과에 영향을 미치지 않는 pure라는 작업을 만든다. 위 로그 작업을 예로 들면, 로그로 빈문자 ""을 추가하는 작업을 pure로 만든다. 그러면 이제야 비로소, 모든 반복된 m 을 join으로 표현할 수 있게 된다

m a --pure--> m (m a) --join--> m a
m (m a) --join--> m a
m (m (m a)) --join--> m (m a) --join--> m a
...

이제, join절차가 항상 있는 m a를 원하는 곳에 m a도 m (m (m a))도 넣어 줄 수 있게 되었다. "hello"와 " world"를 남기던 두 개의 작업 합쳐, "hello world"를 남기는 하나의 작업으로 표현할 수 있게 되었다.

※ 지금 눈에 명확히 보이진 않지만, m 둘을 합성하는 연산을 .이라 하면, .만으론 모노이드 이항 연산 역할을 못하지만, join의 도움을 받고, id 만으론 항등원 역할을 못하지만, pure의 도움을 받아 모노이드 구조를 이룬다.

결론.

당연히 모든 내용이 담겨 있진 않고, 모나드를 무엇의 모노이드로 보는 내용을 비수학적으로 풀어 봤다. 모노이드는 모두를 하나의 모양으로 표현 할 수 있다는 걸, 보증해주는 거대한 개념이지만, 업자인 나에겐 "그렇게 해도 된다"는 정도의 느낌만 있다. (결합 법칙이 빠졌는데, 나중에 코드를 모듈화 하는 것과 연관지어 보면, 명확한 대응을 알 수 있다.)

모나드는, 조금 다르게 생긴 것을, 당장 필요한 요소만 잘 관리한다면 "같은 걸로 치자"를 멋지게(,어렵게) 형식화한 이론이다.

사족.
저와 대화를 나눠본 분들은 아시겠지만, 제가 비전공자라 용어 선택이나 개념 정의가 매우 인포멀해서 인상을 찌푸리는 경우도 자주 만듭니다. PL 전공자분들처럼 깊숙히 이론을 파고 싶은 게 아니라, 현실에 적용할 수 있을 만큼의 눈만 가지고 싶습니다. 현실을 모델링할 때, "인위적 정보 선택"을 해서 필요한 정보를 남길 수 있는 경우를 알아채는 눈을 길러야 되는데, bind 또는 flatmap, return 또는 pure가 있는 구조가 모나드라고만 배우면, 이런 눈을 가지는데 매우 오래 걸리는 것 같습니다.

비전공 업자분이 보셨다면, 얻어 가시는 아이디어가 있었으면 좋겠고, 전공자분이 보셨다면, 인포멀한 부분에 너무 인상 찌푸리지 마시고, 틀린 개념이 있다면, 부드럽게 조언을 해주시면 좋겠습니다.

※ 모나드 용어는 mono와 triad에 온 게 아닐까 의심한다는 설이 있습니다.(검색해 보면 근거는 미약해 보입니다.) 모나드는 join, return 그리고 위에서 명시적 언급은 안했지만, 펑터의 fmap, 이렇게 세 개 triad의 도움을 받아 모노이드로 만들 수 있는 구조입니다.

※ "정교한" 내용이 아님을 강조하고 선입견이 생기지 않기 위해, 일부러 제목을 달지 않고, 반말(혼잣말)투로 썼습니다.

제목은

1. 함수형
2. 모노이드
3. 모나드

순서 입니다.

웹 접근성의 중요성과 WAI-ARIA 표준을 바탕으로 한 의미론적인 UI를 설계한 사례를 블로그에 공개했습니다.

전문성 검증이 필요한 분야이다 보니, 퇴고 과정에 접근성 전문가 @resistan 님의 도움을 받았습니다.

함수형 언어(Functional Language)의 핵심

함수형 언어가 점점 많은 매체에 노출되고, 더 많은 언어들이 함수형 언어의 특징을 하나 둘 받아들이고 있다. 함수형 언어, 적어도 그 특징이 점점 대세가 되고 있다는 이야기이다. 하지만, 함수형 언어가 대체 무엇이란 말인가? 무엇인지도 모르는 것이 대세가 된다고 할 수는 없지 않은가?

함수형 언어란 아주 단순히 말해서 함수가 표현식^[1]인 언어를 말한다. 다른 말로는 함수가 값이기 때문에 다른 함수를 호출해서 함수를 얻어내거나 함수의 인자로 함수를 넘길 수 있는 언어를 말한다. 그렇다면 이 단순화된 핵심만을 포함하는 언어로 함수형 언어의 핵심을 이해할 수 있지 않을까? 이게 바로 람다 대수(Lambda Calculus)의 역할이다.^[2]

람다 대수는 딱 세 종류의 표현식만을 가지고 있다.

1. 변수 (xx, yy, …\ldots)
2. 매개변수 xx에 인자를 받아 한 표현식 MM(함수의 몸체)을 계산하는 함수 (λx→M\lambda x\to M)
3. 어떤 표현식 LL의 결과 함수를 인자 NN으로 호출 (L NL\ N)

이후의 설명에서는 MM 과 NN, 그리고 LL이라는 이름을 임의의 표현식을 나타내기 위해 사용할 것이다. 람다 대수가 어떤 것들을 표현할 수 있는가? 앞에서 말했듯이 람다 대수는 함수의 인자와 함수 호출의 결과가 모두 함수인 표현식을 포함한다. 예를 들어 λx→(λy→y)\lambda x \to (\lambda y \to y) 는 매개변수 xx에 인자를 받아 함수 λy→y\lambda y \to y를 되돌려주는 함수이고, λx→(x (λy→y))\lambda x \to (x\ (\lambda y \to y))는 매개변수 xx에 함수인 인자를 받아 그 함수를 (λy→y\lambda y \to y를 인자로 사용하여) 호출하는 함수이다.

람다 대수(Lambda Calculus)의 평가(Evaluation)

이제 문제는

그래서 람다 대수의 표현식이 하는 일이 뭔데?

이다. 위의 표현식에 대한 소개는 산수로 말하자면 x+yx + y와 같이 연산자(++)와 연산항(xx와 yy)로부터 얻어지는 문법만을 설명하고 있고, 3+53 + 5와 같은 구체적인 표현식을 계산해서 88이라는 결과 값을 내놓는 방식을 설명하고 있지 않다. 이런 표현식으로부터 값을 얻어내는 것을 언어의 "평가 절차"("Evaluation Procedure")라고 한다. 람다 대수의 평가 절차를 설명하는 것은 어렵지 않다. 적어도 표면적으로는 말이다.

• 함수는 이미 값이다.
• 함수 λx→M\lambda x \to M을 NN으로 호출하면 MM에 등장하는 모든 xx을 NN으로 치환(Substitute)하고 결과 표현식의 평가를 계속한다.

이는 겉으로 보기에는 말이 되는 설명처럼 보인다. 하지만 이 설명을 실제로 해석기(Interpreter)로 구현하려고 시도한다면 이 설명이 사실 여러 세부사항을 무시하고 있다는 점을 깨닫게 될 것이다.

1. 함수 호출 L NL\ N에서 LL이 (아직) λx→M\lambda x \to M 꼴이 아닐 때는 어떻게 해야하지?
2. 함수 호출 (λx→M) N(\lambda x \to M)\ N에서 NN을 먼저 평가하는 게 낫지 않나? xx가 MM에 여러번 등장한다면 NN을 여러번 평가해야 할텐데?

첫번째 문제는 비교적 간단히 해결할 수 있다. LL을 먼저 평가해서 λx→M\lambda x \to M 꼴의 결과 값을 얻어낸 뒤에 호출을 실행하면 되기 때문이다. 반면에 두번째 질문은 좀 더 미묘한 문제를 가지고 있다. 함수 호출의 평가에서 발생하는 이 문제에 구체적인 답을 하기 위해서는 값에 의한 호출(Call-By-Value, CBV)와 이름에 의한 호출(Call-By-Name, CBN)이 무엇인지 이해해야 한다.

값에 의한 호출(Call-By-Value)? 이름에 의한 호출(Call-By-Name)?

앞에서 말한 함수 호출에서부터 발생하는 문제는 사실 함수형 언어에서만 발생하는 문제는 아니다. C와 같은 명령형 언어에서도 함수를 호출할 때 인자를 먼저 평가해야하는지를 결정해야하기 때문이다. 즉 이 문제는 함수를 가지고 있고 함수를 호출해야하는 모든 언어들이 가지고 있는 문제이다.

그렇다면 이 일반적인 문제를 어떻게 해결하는가? 대부분의 언어가 취하는 가장 대표적인 방식은 "값에 의한 호출"("Call-By-Value", "CBV")이라고 한다. 이 함수 호출 평가 절차에서는 함수의 몸체에 인자를 치환하기 전에^[3] 인자를 먼저 평가한다. 이 방식을 사용하면 인자를 여러번 평가해야하는 상황을 피할 수 있다.

또 다른 방식은 "이름에 의한 호출"("Call-By-Name", "CBN")이라고 한다. 이 방식에서는 함수의 몸체에 인자를 우선 치환한 후 몸체를 평가한다. 몇몇 언어의 매크로(Macro)와 같은 기능이 이 방식을 사용한다. 얼핏 보기에는 CBN은 장점이 없어보인다. 그러나 함수가 인자를 사용하지 않을 경우는 CBN이 장점을 가진다는 것을 볼 수 있다. 극단적으로 평가가 종료되지 않는 표현식(Non-terminating expression)이 있다면^[4] CBV는 종료하지 않고 CBN만이 종료하는 경우가 있음을 다음 예시를 통해 살펴보자. 표현식 (λx→(λy→y)) N(\lambda x \to (\lambda y \to y))\ N이 있다고 할 때, NN이 평가가 종료되지 않는 표현식이라고 하자. 이 경우 CBV를 따른다면 종료하지 않는 NN 평가를 먼저 수행하느라 이 표현식의 값을 얻어낼 수 없지만, CBN을 따른다면 λy→y\lambda y \to y라는 값을 손쉽게 얻어낼 수 있다. 바로 이런 상황 때문에

CBN은 CBV보다 일반적으로 더 많은 표현식들을 평가할 수 있다

고 말한다.

모호한 선택을 피하는 방법

두 방식의 장점을 모두 가질 수는 없을까? 다시 말해서, 어떤 상황에서는 이름에 의한 호출을 사용하고, 어떤 상황에서는 값에 의한 호출을 사용할 수 없을까? 이 질문에 답한 수많은 선구자들 가운데 폴 블레인 레비(Paul Blain Levy)가 내놓은 답인 "값 밀기에 의한 호출"("Call-By-Push-Value", "CBPV")은 함수형 언어의 평가를 기계 수준(Machine level)에서 이해하는데에 있어 강력한 도구를 제공한다. CBPV는 우선 "계산"("Computation")과 "값"("Value")을 구분한다.

• 계산 MM, NN, LL, …\ldots = 함수 λx→M\lambda x \to M 또는 함수 호출 L VL\ V
• 값 VV, UU, WW, …\ldots = 변수 xx

잠깐, 앞서서 함수형 언어에서 함수는 값이라고 하지 않았던가? 이는 값 밀기에 의한 호출에서 함수와 함수 호출을 종전과 전혀 다르게 이해하기 때문이다. 함수 λx→M\lambda x \to M는 스택(Stack)에서 값을 빼내어(Pop) xx라는 이름을 붙인 후 MM을 평가하는 것이고, 함수 호출 L VL\ V는 스택에 값 VV를 밀어넣고(Push)^[5] LL을 평가하는 것이다. 따라서 함수 λx→M\lambda x \to M는 평가의 결과가 아닌 추가적인 평가가 가능한 표현식이 된다. 이 구분을 간결하게 설명하는 것이 다음의 CBPV 표어이다.

값은 "~인 것"이다. 계산은 "~하는 것"이다.

그렇지만 함수형 언어이기 위해서는 함수를 값으로 취급할 수 있어야 한다고 했지 않은가? 그렇다. 이를 위해 CBPV는

계산을 강제한다면(force\mathbf{force}) 계산 MM를 하는 지연된 계산인 값 thunk(M)\mathbf{thunk}(M)

을 추가로 제공한다. 이 둘 (force(V)\mathbf{force}(V)와 thunk(M)\mathbf{thunk}(M))을 다음과 같이 문법에 추가할 수 있다.

• 계산 = λx→M\lambda x \to M 또는 L VL\ V 또는 force(V)\mathbf{force}(V)
• 값 = xx 또는 thunk(M)\mathbf{thunk}(M)

CBPV를 완성하기 위해 필요한 마지막 조각은 계산을 끝내는 법이다. 현재까지 설명한 λx→M\lambda x \to M와 L VL\ V 그리고 force(V)\mathbf{force}(V) 는 모두 다음 계산을 이어서 하는 표현식이고, 계산을 끝내는 방법을 제공하지는 않는다. 예를 들어 λx→M\lambda x \to M의 평가는 스택에서 값을 빼내고 계산 MM의 평가를 이어한다. 그렇다면 계산의 끝은 무엇인가? 결과 값을 제공하는 것이다. 이를 위해 return(V)\mathbf{return}(V)를 계산에 추가하고, 이 결과 값을 사용할 수 있도록 M to x→NM\ \mathbf{to}\ x \to N (계산 MM을 평가한 결과 값을 xx라고 할 때 계산 NN을 평가하는 계산) 또한 계산에 추가하면 다음의 완성된 CBPV를 얻는다.

• 계산 = λx→M\lambda x \to M 또는 L VL\ V 또는 force(V)\mathbf{force}(V) 또는 return(V)\mathbf{return}(V) 또는 M to x→NM\ \mathtt{\mathbf{to}}\ x \to N
• 값 = xx 또는 thunk(M)\mathbf{thunk}(M)

이제 CBPV를 얻었으니 원래의 목표로 돌아가보자. 어떻게 CBV 호출과 CBN 호출을 CBPV로 설명할 수 있을까?

• CBV 함수 λx→M\lambda x \to M와 호출 L NL\ N이 있다면, 이를 return(thunk(λx→M))\mathbf{return}{(\mathbf{thunk}(\lambda x \to M))}과 L to x→N to y→force(x) yL\ \mathbf{to}\ x \to N\ \mathbf{to}\ y \to \mathbf{force}(x)\ y로 표현할 수 있다. 즉, CBPV의 관점에서 CBV의 함수는 지연된 원래 계산 λx→M\lambda x \to M을 값으로 되돌려주는 계산으로 이해할 수 있고, 함수 호출 L NL\ N은 함수 부분 LL을 먼저 평가하고 NN을 평가한 뒤 NN의 계산 결과 yy를 스택에 밀어넣고 지연된 계산인 함수 부분 xx의 계산을 강제하는(force(x)\mathbf{force}(x)) 것으로 이해할 수 있다.
• CBN 함수 λx→M\lambda x \to M와 호출 L NL\ N이 있다면, 이를 λx→M\lambda x \to M(단, 변수 xx의 모든 사용을 force(x)\mathbf{force}(x)로 치환함)과 L thunk(N)L\ \mathbf{thunk}(N)로 표현할 수 있다. 즉, CBPV의 관점에서 함수 호출은 L NL\ N은 지연된 NN을 스택에 밀어넣은 뒤 LL의 계산을 이어가는 것으로 볼 수 있다. 이 지연된 NN은 이후에 스택에서 빼내어져 어떤 이름 xx가 붙은 뒤, 이 변수가 사용될 때에야 비로소 계산된다.

다소 설명이 복잡할 수 있으나, 단순하게 말해서 CBPV는 CBV에 따른 상세한 평가 순서와 CBN 따른 상세한 평가 순서를 세부적으로 설명할 수 있는 충분한 기능을 모두 갖추고 있으며, 이를 통해 CBV 함수 호출과 CBN 함수 호출을 모두 설명할 수 있다는 이야기이다.

기계 수준(Machine level)에서의 Call-By-Push-Value의 장점

앞에서는 CBPV가 CBV와 CBN를 모두 설명할 수 있음을 다뤘다. 그러나 CBPV는 프로그래머(Programmer)가 직접 사용하기에는 과도하게 자세한 세부사항들을 포함하고 있기에, 프로그래머가 직접 CBPV를 써서 CBV와 CBN의 구분을 조율하기에는 적합하지 않다. 그렇다면 어느 수준에서 CBV와 CBN을 혼합해 사용할 때 도움을 줄 수 있을까? 바로 람다 대수를 기계 수준으로 컴파일(Compile)할 때이다. 이때는 CBPV가 가진 자세한 세부사항의 표현력이 굉장히 유용해진다.

예를 들어 람다 대수를 기계 수준으로 변환할 때 흔히 필요한 것 중 하나인 항수 분석(Arity analysis)에 대해 이야기해보자. 항수 분석은 함수가 하나의 인자를 받은 뒤 실행되어야 하는지, 혹은 두 인자를 모두 받아 실행되어야 하는지 등을 확인하여 이후에 그에 걸맞는 최적화된 기계어(Machine language)를 생성할 수 있게 도와주는 분석 작업이다. 평범한 람다 대수에서는 항수 분석의 결과를 직접적으로 표현하기 어렵다. 예를 들어 람다 대수의 λx→(λy→y)\lambda x \to (\lambda y \to y)의 경우 이 함수가 xx와 yy를 모두 받아 yy를 되돌려주는 함수인지 (항수가 2인 함수인지), 혹은 xx를 받아 λy→y\lambda y \to y라는 함수를 되돌려주는 함수인지 (항수가 1인 함수인지) 구분할 수 없다. 그러나 이를 CBPV로 변환한 λx→(λy→return(y))\lambda x \to (\lambda y \to \mathtt{return}(y))나 λx→return(thunk(λy→return(y)))\lambda x \to \mathtt{return}(\mathtt{thunk}(\lambda y \to \mathtt{return}(y)))는 각각이 무엇을 뜻하는지 분명히 이해할 수 있다.

• λx→(λy→return(y))\lambda x \to (\lambda y \to \mathtt{return}(y))는 두 변수 xx와 yy를 스택에서 빼낸 뒤 yy의 값을 되돌려주는 함수(항수가 2인 함수)이다.
• λx→return(thunk(λy→return(y)))\lambda x \to \mathtt{return}(\mathtt{thunk}(\lambda y \to \mathtt{return}(y)))는 변수 xx를 스택에서 빼낸 뒤 지연된 계산 λy→return(y)\lambda y \to \mathtt{return}(y)를 돌려주는 함수(항수가 1인 함수)이다.

이런 장점을 바탕으로 CBPV를 더 발전시킨 "언박싱한 값에 의한 호출"("Call-By-Unboxed-Value")을 GHC 컴파일러의 중간 언어(Intermediate language)로 구현하는 것에 대한 논의가 현재 진행되고 있으며 앞으로 더 많은 함수형 컴파일러들이 관련된 중간 언어를 채용하기 시작할 것으로 보인다.

마치며

이 글에서는 함수형 언어의 핵인 람다 대수를 간단히 설명하고 람다 대수를 평가하는 방법에 대해서 다루어보았다. 특히 그 중 값 밀기에 의한 평가(Call-By-Push-Value, CBPV)가 무엇이며 CBPV가 다른 대표적인 두 방법(CBV, CBN)을 어떻게 표현할 수 있는지, 그리고 CBPV의 장점이 무엇인지에 대해서도 다루어 보았다. 이 글에서 미처 다루지 못한 중요한 주제는 CBPV를 기계에 가까운 언어로 번역해보는 것이다. 여기에서는 글이 너무 복잡해지는 것을 피하기 위해 제했으나, CBPV의 장점에서 살펴봤듯 이는 CBPV에 있어 핵심 주제 중 하나이기 때문에 이후에 다른 글을 통해서라도 이 주제를 소개할 기회를 가지고자 한다. 이 글이 CBPV에 대한 친절한 소개글이었기를 바라며 이만 줄이도록 하겠다.

---

1. 결과 값(Value)을 가지는 언어 표현을 말한다. 예를 들어 1+11 + 1은 22라는 값을 가지는 표현식이지만 (JavaScript의) let x = 3;나 (Python의) def f(): ...은 그 자체로는 값이 없기 때문에 표현식이 아니다. ↩︎

2. 다만 실제 역사에서는 람다 대수의 이해와 발견이 함수형 언어의 개발보다 먼저 이루어졌다. 이런 역사적 관점에서는 (이미 많은 수학자들이 이해하고 있던) 람다 대수에 여러 기능을 추가한 것이 바로 함수형 언어라고 볼 수 있다. ↩︎

3. 프로그래밍 언어(Programming Language)는 실제로는 치환을 사용하지 않고 환경(Environment)을 사용하는 경우가 더 많지만 설명의 편의를 위해 다른 언어들 또한 환경 대신 치환에 기반해 평가한다고 가정하겠다. ↩︎

4. 앞서 설명한 람다 대수에서는 이를 쉽게 얻을 수 있다. 오메가(Ω\Omega)라고 부르는 표현식인 (λx→x x) (λx→x x)(\lambda x \to x\ x)\ (\lambda x \to x\ x)의 평가는 값에 의한 호출을 따르든 이름에 의한 호출을 따르든 종료되지 않는다. ↩︎

5. 바로 이 함수 호출을 값 밀기에 기반해 해석하는 데에서 CBPV의 이름이 유래했다. ↩︎

같은 것과 같지 않은 것

국밥 두 그릇의 가격이 얼마인가? KTX의 속력이 몇 km/h인가? 내일 기온은 몇 도인가? 일상에서 묻는 이런 질문은 항상 같음의 개념을 암시적으로 사용하고 있다. 앞의 예시를 보다 명시적으로 바꾼다면 아래와 같이 (다소 어색하게) 말할 수 있다.

• 국밥 두 그릇의 가격은 몇 원과 같은가?
• KTX의 속력은 몇 km/h와 같은가?
• 내일 기온은 몇 도와 같은가?

이런 질문들의 추상화인 이론들은 자연스럽게 언제 무엇과 무엇이 같은지에 대해서 답하는 데에 초점을 맞추게 된다. 예를 들면

• x2+x+1=0x^2 + x + 1 = 0의 실수 해의 갯수는 0과 같다.
• 물 분자 내의 수소-산소 연결 사이의 각도는 104.5도와 같다.
• 합병 정렬의 시간 복잡도는 O(nlog⁡n)O(n\log{n})과 같다.

등이 있다. 이렇게 어떤 두 대상이 같은지에 대해서 이야기를 하다보면 반대로 어떤 두 대상이 같지 않은지에 대해서도 이야기하게 된다. 즉,

• x+4x + 4를 22로 나눈 나머지는 x+1x + 1을 22로 나눈 나머지와 같지 않다.
• 연결 리스트(Linked List)와 배열(Array)은 같지 않다.
• 함수 λ x→x\lambda\ x \to x와 정수 55는 같지 않다.

같은 것과 판정 문제(Decision Problem)

이제 컴퓨터 과학(Computer Science)과 프로그래밍(Programming)에 있어 자연스러운 의문은 "두 대상이 같은지 아닌지와 같은 답을 주는 알고리즘(Algorithm)이 있나?"일 것이다. 다시 말해서 두 대상 aa와 bb를 입력으로 주었을 때

• 알고리즘이 참 값(True\mathtt{True})을 준다면 aa와 bb가 같고
• 알고리즘이 거짓 값(False\mathtt{False})을 준다면 aa와 bb가 같지 않은

알고리즘이 있는지 물어볼 수 있다. 이런 어떤 명제가 참인지 거짓인지 판정하는 알고리즘의 존재 여부에 대한 질문을 "판정 문제"("Decision Problem")라고 하며, 명제 PP에 대한 판정 문제에서 설명하는 알고리즘이 존재한다면 "PP는 판정 가능하다"("PP is decidable")고 한다. 즉, 앞의 질문은 "임의의 aa와 bb에 대해 aa와 bb가 같은지 판정 가능한가?"라는 질문과 같은 의미라고 할 수 있다.

이 질문에 대한 대답은 당연하게도 어떤 대상을 어떻게 비교하는지에 따라 달라진다. 예를 들어 우리가 32 비트(bit) 정수에 대해서만 이야기하고 있다면 "임의의 32 비트 정수 aa와 bb에 대해 aa와 bb가 각 비트별로 같은지 판정 가능한가?"라는 질문에 대한 답은 "그렇다"이다. 반면 우리가 비슷한 질문을 자연수를 받아 자연수를 내놓는 임의의 함수에 대해 던진다면 답은 "아니다"가 된다.^[1]

그렇다면 어떤 대상의 어떤 비교에 대해 판정 문제를 물어보아야할까? 프로그래머(Programmer)로서 명백한 대답은 두 프로그램(Program)이 실행 결과에 있어서 같은지 보는 것일 것이다. 그러나 앞서 자연수를 받아 자연수를 내놓는 함수에 대해 말했던 것과 비슷하게 두 프로그램의 실행 결과를 완벽하게 비교하는 알고리즘은 존재하지않는다. 이는 우리가 두 프로그램의 같음을 판정하고 싶다면 그 같음을 비교하는 방법에 제약을 두어야 함을 말한다. 여기서는 다음의 두 제약을 대표로 설명할 것이다.

1. 문법적 비교(Syntactic Comparison)
2. β\beta 동등성 (β\beta Equivalence)

1. 문법적 비교(Syntactic Comparison)

이 방법은 말 그대로 두 프로그램이 문법 수준에서 같은지를 보는 것이다. 예를 들어 다음의 두 JavaScript 프로그램은 문법적으로 같은 프로그램이다.

// 1번 프로그램
let x = 5;
console.log(x);

// 2번 프로그램
let x  =  5;
console.log( x );

공백문자의 사용에서 차이가 있으나, 그 외의 문법 요소는 모두 동일함에 유의하자. 반면 다음의 두 JavaScript 프로그램은 동일한 행동을 하지만 문법적으로는 다른 프로그램이다.

// 1번 프로그램
let x = 5;
console.log(x);

// 2번 프로그램
let x = 3 + 2;
console.log(x);

두 프로그램 모두 x에 5라는 값을 할당하고 5를 콘솔에 출력하나, 첫번째 프로그램은 = 5;를, 두번째 프로그램은 = 3 + 2을 사용하여 5를 할당하고 있기 때문에 문법적으로 다르다.

문법적 비교는 이렇게 문법만 보고서 쉽게 판정할 수 있다는 장점이 있으나, 두번째 예시처럼 쉽게 같은 행동을 함을 이해할 수 있는 프로그램에 대해서도 "같지 않음"이라는 결과를 준다는 단점을 가진다. 혹자는

3 + 2같은 계산은 그냥 한 다음에 비교하면 안돼? 컴파일러(Compiler)도 상수 전파(Constant Propagation) 최적화라던지로 3 + 2를 5로 바꾸잖아?

라는 생각을 할 수도 있을 것이다. 이 제안을 반영한 방법이 바로 β\beta 동등성이다.

2. β\beta 동등성

바로 앞의 소절에서 단순 계산의 추가에 의해 같음이 같지 않음으로 변하는 것을 보았다. 이런 상황을 피하기 위해서는 같음을 평가할 때 프로그램의 실행을 고려하도록 만들어야 한다. 가장 대표적인, 대부분의 프로그래밍 언어(Programming Language)에 존재하는 프로그램의 실행은 함수 호출이다. 따라서 함수 호출을 고려한 같음의 비교는 f(c)와 함수 f의 몸체 b 안에서 인자 x를 c로 치환한 것을 같다고 취급해야한다. 예를 들어

let f = (x) => x + 3;

이 있다면, f(5)와 5 + 3 혹은 8을 같은 프로그램으로 취급해야한다. 이 비교 방법의 큰 문제는 함수가 종료하는지 알지 못한다는 것이다. 두 프로그램 a와 b를 비교하는데, a가 종료하지 않는 함수 l을 호출한다면, 이 알고리즘은 "같음"이나 "같지 않음"이라는 결과를 낼 수조차 없다. 즉, 올바른 판정법이 될 수 없다.

더 심각한 문제는 아직 값을 모르는 변수가 있는 "열린 프로그램"("Open Program")에 대해서도 이런 계산을 고려해야한다는 것이다. 다음의 JavaScript 예시를 보자.

let g = (x) => f(x) + 3;
let h = (x) => (x + 3) + 3;

g와 h는 같은 프로그램일까? 우리가 g와 h가 같은 프로그램이기를 원한다면 f(x)와 x + 3을 같은 프로그램으로 보아야한다. 대부분의 프로그램은 함수 안에서 쓰여지기 때문에 프로그램의 비교는 거의 항상 g와 h의 몸체와 같은 열린 프로그램들의 비교이다. 따라서 g와 h를 다른 프로그램으로 본다면 계산을 실행하여 두 프로그램을 비교하는 의미가 퇴색되고 만다. 그렇기 때문에 우리는 x와 같이 값이 정해지지 않은 변수가 있을 때에도 f(x)을 호출하여 비교해야만 한다. 이는 우리가 단순히 모든 함수가 종료하는지 여부를 떠나서, 함수의 몸체에 등장하는 모든 부속 프로그램(Sub-program)이 종료하는지 아닌지를 따져야만 한다는 이야기이다.

이런 강한 제약조건으로 인해 β\beta 동등성을 통해서 프로그램 비교의 판정 문제를 해결 가능한 곳은 매우 제한적이지만, β\beta 동등성이 매우 유용한 한가지 경우가 있다. 바로 의존 형이론(Dependent Type Theory)의 형검사(Type Checking)이다.

의존 형이론과 형의 같음

의존 형이론은 형(Type)에 임의의 프로그램을 포함할 수 있도록 하는 형이론(Type Theory)의 한 종류이다. 예를 들어 명시적인 길이(n)를 포함한 벡터(Vector) 형을 Vector n Int과 같이 쓸 수 있다. 이 형은 n개의 Int값을 가진 벡터를 표현하는 형이다. 이제 append라는 두 벡터를 하나로 연결하는 함수를 만든다고 해보자. 대략 다음과 같은 형을 쓸 수 있을 것이다.

append : Vector n a -> Vector m a -> Vector (n + m) a

즉, append는 길이 n짜리 a 형의 벡터와 길이 m짜리 a 형의 벡터를 합쳐서 길이 n + m짜리 a 형의 벡터를 만드는 함수이다. 이 함수를 사용해서 길이 5의 벡터를 길이 2와 길이 3짜리 벡터 x, y로부터 만들고 싶다고 하자.

append x y : Vector (2 + 3) a

안타깝게도 우리는 길이 2 + 3짜리 벡터를 얻었지, 길이 5짜리 벡터를 얻진 못했다. 여기서 앞서의 질문이 다시 돌아온다.

아니, 2 + 3를 5로 계산하면 되잖아?"

그렇다. 이런 의존 형에 β\beta 동등성을 적용하면 우리가 원하는 형을 바로 얻어낼 수 있다. Vector (2 + 3) a과 Vector 5 a는 같은 형이기 때문이다. 더욱이, 의존 형의 경우 종료하지 않는 부속 프로그램이 잘못된 형을 줄 수 있기 때문에 많은 경우 종료하지 않는 부속 프로그램을 어차피 포함하지 않는다. 다시 말해, 앞서 말한 제약 조건 즉 모든 부속 프로그램이 종료해야만 한다는 제약조건은 의존 형의 경우 상대적으로 훨씬 덜 심각한 제약조건이 되는 것이다.

이런 의존 형에 있어서의 β\beta 동등성 검사를 "변환 검사"("Conversion Check")라고 하며, 두 형이 β\beta 동등일 경우 이 두 형이 서로 "변환 가능하다"("Convertible")라고 한다. 이 변환 검사는 의존 형이론 구현에 있어서 가장 핵심인 기능 중 하나이며, 가장 잦은 버그를 부르는 기능 중 하나이기도 하다.

마치며

이 글에서는 같음과 같지 않음의 판정 문제에 대해 간략히 설명하고 프로그램의 같음을 판정하는 법에 대해서 단순화하여 다루어보았다. 구체적으로는 문법 기반의 비교와 β\beta 동등성을 통한 비교로 프로그램의 같음을 판정하는 법을 알아보았고, 이 중 β\beta 동등성이 적용되는 가장 중요한 예시인 의존 형이론을 β\beta 동등성을 중점으로 짤막하게 설명하였다. 마지막 문단에서 언급했듯 의존 형이론의 구현에 있어서 β\beta 동등성을 올바르게 구현하는 것은 가장 중요한 작업 중 하나이기에, 최근 연구들은 β\beta 동등성의 구현 자체를 의존 형이론 안에서 함으로서 검증된 β\beta 동등성의 구현을 하기 시작하고 있다. 이 글이 같음과 같지 않음과 판정 문제 그리고 β\beta 동등성에 있어 유용한 설명을 내놓았기를 바라며 이만 줄이도록 하겠다.

---

1. 두 함수가 같다라고 보는 방법에 따라 다르나, 두 함수가 항상 같은 값을 가진다면 같다고 하자. 이때 함수의 판정 문제는 정지 문제(Halting Problem)와 동일하다. 임의의 튜링 기계(Turing Machine) ff가 입력 nn을 받았을 때 종료하면 g(n)=1g(n) = 1, 아니면 g(n)=0g(n) = 0이라고 하면 이 함수 gg와 상수 함수 c(n)=1c(n) = 1가 같은 함수임을 보이는 것은 ff가 항상 종료한다는 것을 보이는 것과 동등하다. ↩︎