관계적 유형 이론과 함수적 유형 이론 간의 번역?

논리학
1

철학적 논리학에서 통용되는 유형 이론(type theory)의 짜임에는 다음의 두 형태가 있는 것으로 알려져 있습니다:

  1. 함수적 유형 이론: e (이름형), t (문장형)를 기본 유형으로 지니고, 𝜏와 𝜎가 유형일 때, 𝜏→𝜎는 𝜏 유형의 논항을 받아 𝜎 유형의 논항을 내놓는 함수적 유형으로 이해됨.
  2. 관계적 유형 이론: e (이름형)만을 기본 유형으로 지니고, 𝜏가 유형일 때, ⟨𝜏⟩는 𝜏 유형의 논항을 받아 문장을 내놓는 관계적 유형으로 이해됨. 한편, 이 경우 빈 튜플 ⟨⟩은 그 자체로 문장형에 상당하는 것이 됨.

그리고 도어(Cian Dorr)의 2016년 논문, “To be F is to be G”의 부록 A2에 따르면 두 유형 이론은 상호 번역 가능하다고 하는데요.

그런데 정말 그런지를 잘 모르겠습니다. 가령, 함수적 유형 이론에서 우리는 e→e 타입, 말하자면 일차 함수 타입을 정의할 수 있습니다. 그런데 관계적 유형 이론에서 이런 유형이 어떻게 정의될 수 있는 것인가요?

도어에 따르면 (그의 표기법에 따라 덜 엄밀한? 듯한... 콤비네이터 언어를 사용해 표기합니다) 다음의 동치가 성립하므로 함수적 이론과 관계적 이론 간의 번역이 가능하다는 건데요 (원문은 우변의 알파벳 위치가 반대인데 제 생각에 키안의 실수로 보입니다):

𝜏→𝜎 ≡ ⟨𝜎⟩𝜏

이에 따르면 e→e 유형은 관계적 언어에서 다음과 같은 타입으로 이해될 텐데

⟨e⟩e

이건 그냥 이름형을 받아 술어 유형의 표현을 내놓는 함수 아닌가요? 이는 e→e로써 표현되는, 일차 함수의 유형과는 아주 상이해 보입니다. (아니면 도어가 ⟨𝜎⟩𝜏를 통해 의도하는 게 제가 이해하는 것과 다른 것인지도….)

그래서 다시 질문은… ‘어떻게 관계적 유형 이론에서 일차 함수를 표현할 수 있는가?’입니다. 유형 이론에 잔뼈가 굵은 분께서 도와주시길 소망합니다.

(아마도… @chabulhwi 님께 도움을 받을 수 있으리라 기대하는 중…)

4개의 좋아요
2

위의 논문 중 부록 A1과 A2의 초반부만 대충 읽어 봤는데, 저는 유형론을 제대로 배운 적이 없는 사람임을 먼저 밝힐게요.

부록 A2의 정의 2.1에 있는 𝜏 ≠ 𝑒라는 조건 때문에, @car_nap 님의 위의 말씀이 맞는지 잘 모르겠어요.

ℱ—the set of functional types—is the smallest set containing the letters ‘𝑒’ (the type of objects) and ‘𝑡’ (the propositional type—think ‘truth evaluable’, not ‘truth value’), such that whenever 𝜎 and 𝜏 belong to it and 𝜏 ≠ 𝑒, the ordered pair ⟨𝜎, 𝜏⟩—which we write as (𝜎 → 𝜏)—belongs to it. (65쪽)

근데 𝜏 ≠ 𝑒라는 조건이 위의 정의에 왜 들어 있는지도 저는 이해가 잘 안 가네요.

그리고 사실 '관계적 유형론'이나 '함수적 유형론'을 저는 이 글에서 처음 봤어요. :sweat_smile:

2개의 좋아요
3

엇 제가 본 버전과 약간 다르네요. 링크 감사합니다!

1개의 좋아요
4

음, 제가 위의 논문을 정독하지도 않고 감히 추측해 볼게요. 관계형 ⟨α, β⟩는 함수형 α → (β → 𝑡)로 이해할 수 있죠? 그 반대도 성립하고요.

그래서 왠지 𝜏 → 𝜎 = ⟨𝜏⟩ ⌢ 𝜎일 듯하네요. 65쪽에 다음 등식이 나오네요.

(𝜎 → 𝜏) ^ ℱ = ⟨𝜎 ^ ℱ⟩ ⌢ (𝜏 ^ ℱ)

여기서 ⌢는 튜플의 연결을 가리킨대요.

66쪽에 그 이유가 나와 있군요.

Note that it is crucial to this result that ℱ does not contain any types of the
form 𝜏 → 𝑒: if we had allowed for these, we would have something richer than ℛ. (66쪽)

그래도 저는 약간 의아하네요. 𝜏 → 𝑒 꼴의 함수형에 대응하는 관계형을 ℛ에 추가하면 되지 않나 싶어서요. 뭐, 이 선택은 제가 해당 저자의 논문을 충분히 읽으면 이해할 수도 있겠죠?

1개의 좋아요
5

아, 웹 버전에서 저 눈썹 기호가 없어서 콤비네이터 언어를 이상하게 쓴 줄 알았네요. 말씀이 맞는 것 같습니다. 𝜎→𝜏 = ⟨𝜎, 𝜏⟩라는 말이었네요.

1개의 좋아요
6

수식 지원의 중요성이 여기서 드러나는군요...!

1개의 좋아요
7

아마 이 부분은, e와 ⟨⟩만을 기본 유형으로 두려는 의도에 의한 것이지 싶어요. 𝜏→e에 대응되는 기본 유형이 어떻게 정의 가능할지도 잘 모르겠네요.

8

위의 논문에서 저자가 도입한 표기법을 무시하고, 제가 그냥 다른 표기법을 하나 만들어 볼게요. [a₀, a₁, a₂, …, aₙ]은 n-튜플을 가리킵니다.

함수형의 집합 ℱ에 σ → 𝑒 꼴의 함수형을 추가한 '확장된 함수형 집합'을 ℱ*로 나타낼게요. 그리고 이와 비슷하게 정의된 '확장된 관계형 집합'을 ℛ*로 나타낼게요.

이제 함수 f : ℱ* → ℛ*를 다음과 같이 정의할게요.

f(𝑒) = 𝑒
f(𝑡) = 𝑡
f(σ → 𝑒) = [f(σ), 𝑒]
f(σ → 𝑡) = [f(σ), 𝑡]
f(σ → (τ → υ)) = [f(σ)] ⌢ f(τ → υ)

위의 정의에 따라, 다음이 성립합니다.

f(𝑒 → 𝑒) = [f(𝑒), 𝑒] = [𝑒, 𝑒]
f(𝑒 → (𝑒 → 𝑒)) = [f(𝑒)] ⌢ f(𝑒 → 𝑒) = [𝑒] ⌢ [𝑒, 𝑒] = [𝑒, 𝑒, 𝑒]
f((𝑒 → 𝑒) → 𝑒) = [f(𝑒 → 𝑒), 𝑒] = [[𝑒, 𝑒], 𝑒]

제가 잘못 정의했을 수도 있어요. 정의를 만들기가 제 예상보다 그리 쉽지 않았네요.

논문 저자의 표기법에 따르면, 관계형 [τ₀, τ₁, τ₂, …, τₙ, 𝑡]는 ⟨τ₀, τ₁, τ₂, …, τₙ⟩과 같이 나타낼 수 있어요. 하지만 관계형 [τ₀, τ₁, τ₂, …, τₙ, 𝑒]를 논문 저자의 표기법으로 나타내지는 못할 거예요.

1개의 좋아요