TL;DR

  • 연산 의미론을 호모토피 n-절단으로 사상하는 의미 실현 함수에서 두 기계의 의미가 동치여도 구현 자체는 동치가 아닐 수 있음.
  • 기계·프로그램·에이전트 같은 실행 시스템을 ∞-범주로 두고, 연산 의미론에 n-절단 함수를 합성해 의미 실현 함수 Qₙ을 정의함.
  • 절단은 일반적으로 국소화이며 동치성을 반영하지 않으므로, 의미 클래스가 같아도 실현은 서로 다를 수 있음.
  • 유한 명세를 만족하는 모든 실현은 하나의 의미 연산 클래스에 속하지만, 실현 범주가 수축 가능하거나 모든 객체가 동치라고 결론 내릴 수는 없음.
  • 추적, 기계 타임라인의 공종성, 재귀적 자기 개선은 의미 수준에서 다룰 수 있으며, 의미 클래스의 유일성이 기계 구현의 유일성을 뜻하지는 않음.

의미 실현

  • 객체가 기계, 프로그램, 에이전트 등 실행 가능한 시스템인 ∞-범주 𝒞와, 이를 ∞-토포스 𝒳로 보내는 연산 의미론 Op: 𝒞 → 𝒳를 둠.
  • n ≥ −2에 대해 n-절단 함수 τ≤n: 𝒳 → 𝒳≤n을 정의하고, 의미 실현 함수 Qₙ := τ≤n ∘ Op: 𝒞 → 𝒳≤n을 둠.
  • 실현 M, N에 대해 Qₙ(M) ≃ Qₙ(N)이면 M ≡ₙ N으로 쓰며, 이를 n 수준의 의미 동치라고 부름. 이는 선택한 호모토피 n-타입으로 사상한 뒤 구별되지 않는 실현을 식별함.
  • 실현 M의 n-의미 클래스 [M]ₙ은 Qₙ(M)이 𝒳≤n의 적절한 호모토피 범주에서 결정하는 동치류임.
  • 따라서 실현에서 의미 클래스로의 사상은 M ∈ 𝒞 ↦ [M]ₙ ∈ π₀(𝒳≤n)임.

실현의 비유일성

  • 함자 F: 𝒞 → 𝒟는 𝒞의 모든 사상 f에 대해 F(f)가 동치이면 f도 동치일 때 보수적이라고 정의함. 이는 F가 동치성을 반영한다는 뜻임.
  • Qₙ(M) ≃ Qₙ(N)이면서 M ≄ N인 실현 M, N이 존재하면 [M]ₙ = [N]ₙ이지만 두 실현은 동치가 아님.
  • 따라서 고려 중인 실현의 부분범주에서 Qₙ이 동치성을 반영하지 않으면 의미적 유일성은 실현의 유일성을 함의하지 않음.
  • 증명은 정의에서 바로 따름. Qₙ(M) ≃ Qₙ(N)은 두 실현이 같은 의미 n-클래스에 속함을 뜻하고, M ≄ N은 실현 범주에서 서로 동치가 아님을 뜻함. 국소화된 의미 범주의 같은 객체에 𝒞의 서로 동치가 아닌 실현이 둘 이상 대응함.
  • 이 결론은 표현이 문자 그대로 다를 수 있다는 것보다 강함. 기계 범주 자체의 동치로 몫을 취한 뒤에도 실현들이 서로 동치가 아닐 수 있으므로, 차이는 단순한 구문상의 차이에 그치지 않음.

절단이 비유일성을 허용하는 이유

  • n ≥ −1일 때 절단 함수 τ≤n: 𝒳 → 𝒳≤n는 일반적으로 동치성을 반영하지 않음.
  • ∞-범주 𝒮의 공간에서 X = Sⁿ⁺¹, Y = ∗를 두면 표준 사상 Sⁿ⁺¹ → ∗은 n-절단 후 동치가 됨. 즉 τ≤n Sⁿ⁺¹ ≃ τ≤n ∗ ≃ ∗임.
  • 그러나 Sⁿ⁺¹ ≄ ∗임. πₙ₊₁(Sⁿ⁺¹) ≅ ℤ이고 πₙ₊₁(∗) = 0이기 때문임.
  • 따라서 절단 의미에서의 동치는 n차보다 높은 모든 호모토피 정보를 잊으며, τ≤n X ≃ τ≤n Y가 X ≃ Y를 함의하지 않음.

유한 명세의 실현

  • 연산의 유한 표현을 P라 하고, 이를 실현하는 전체 부분 ∞-범주를 Real(P) ⊆ 𝒞로 둠.
  • 명세가 의미 n-타입 pP ∈ 𝒳≤n을 결정하고 모든 M ∈ Real(P)에 대해 Qₙ(M) ≃ pP라고 가정함.
  • 이 가정 아래 P는 유일한 의미 연산 클래스 [P]ₙ := pP를 결정함. 임의의 M, N ∈ Real(P)에 대해 Qₙ(M) ≃ pP ≃ Qₙ(N)임.
  • 이 결과는 Real(P)가 수축 가능하거나 모든 객체가 서로 동치임을 뜻하지 않음. 그런 결론에는 예를 들어 Qₙ이 Real(P)에서 보수적이라는 추가 가정이 필요함.
  • M, N ∈ Real(P) 중 M ≄ N인 쌍이 존재하면 Qₙ(M) ≃ Qₙ(N) ≃ [P]ₙ임. 따라서 명세의 의미 연산 클래스는 하나지만 동치가 아닌 기계 실현은 적어도 둘임.

추적과 연산 클래스

  • 실행 가능한 추적의 공간을 Trace라 하고, 연산 의미론의 추적 함수 tr: 𝒞 → Trace와 추적을 의미 클래스로 보내는 의미 재구성 함수 classₙ: Trace → 𝒳≤n을 둠.
  • Qₙ = classₙ ∘ tr이므로 실현은 M ↦ tr(M) ↦ [M]ₙ의 합성으로 표현됨. 추적은 연산 객체이며, classₙ은 실행 추적을 의미 연산 클래스로 변환함.
  • classₙ(tr(M)) ≃ classₙ(tr(N))이어도 고려 중인 실현에서 합성 함수 Qₙ = classₙ ∘ tr이 보수적이지 않다면 M ≃ N이라고 결론 내릴 수 없음.

실현의 공종성

  • I를 방향화된 지표 범주로 두고 기계 타임라인 M: I → 𝒞를 둠.
  • 타임라인이 Real(P)에서 n-공종이라는 조건은 모든 R ∈ Real(P)에 대해 Qₙ(Mᵢ) ≃ Qₙ(R)인 i ∈ I가 존재한다는 뜻임.
  • Real(P) ≠ ∅이고 타임라인이 n-공종이면, 어떤 i ∈ I에 대해 Qₙ(Mᵢ) ≃ [P]ₙ임.
  • 증명에서는 R ∈ Real(P)를 하나 선택함. n-공종성에 따라 Qₙ(Mᵢ) ≃ Qₙ(R)인 i가 존재하고, R이 P의 실현이므로 Qₙ(R) ≃ [P]ₙ임. 따라서 해당 단계의 기계는 선택한 호모토피 n-타입 수준에서 명세를 실현함.

재귀적 자기 개선

  • 에이전트 연산의 n-절단 ∞-타입을 𝒪ₙ := τ≤n𝒪라 하고, 자기 개선이 내부 자기 사상 F: 𝒪ₙ → 𝒪ₙ을 유도한다고 가정함.
  • 초기 의미 연산 o₀ ∈ 𝒪ₙ에서 oₖ₊₁ := F(oₖ)로 재귀적으로 정의하면 oₖ = Fᵏ(o₀)임.
  • 기계족 (Mₖ)ₖ≥₀가 이 과정을 n 수준에서 실현한다는 조건은 모든 k에 대해 Qₙ(Mₖ) ≃ oₖ임. Mₖ₊₁ ≃ Mₖ일 필요는 없음.
  • Qₙ의 섬유가 자명하지 않다면 Qₙ(Mₖ) ≃ oₖ를 만족하는 서로 동치가 아닌 실현이 여럿 존재할 수 있음.
  • 따라서 재귀적 자기 개선은 유일하게 정해진 기계 표현의 자기 사상이라기보다 의미 클래스에 대한 연산 𝒪ₙ → 𝒪ₙ으로 다루는 것이 자연스러움.

주요 결론

  • 유한 명세에서 의미 연산 클래스 [P]ₙ이 결정되고, 그 아래 서로 동치가 아닐 수도 있는 여러 실현 M이 존재할 수 있음.
  • M ↦ Qₙ(M)은 의미적 국소화임. 관련 실현 범주에서 이 사상이 보수적이지 않으면 Qₙ(M) ≃ Qₙ(N)은 M ≃ N을 함의하지 않음.
  • 적절한 유일성 주장은 연산 클래스가 n-동치까지 유일하다는 것임. 그 클래스의 기계 실현은 유일하지 않을 수 있음.
  • 이 비유일성은 서로 다른 구문 표현을 비교하는 데서만 생기는 현상이 아니라, 실현에서 절단된 의미 국소화로 넘어갈 때 발생하는 구조적 결과임.