자연수에 대한 초기 대수

Question

나는 자연수의 기본 사례를 사용하여 초기 대수와 catamorphism 개념을 이해하도록 노력하고 있지만 분명히 뭔가를 놓치고 있습니다 (또한 내 Haskell 구문이 엉망 일 수 있습니다).

나중에 편집

내 문제는 주로 기능과 관련된 생각 Fx/ unFix사이의 동형를 정의 NatF (Fix NatF)하고 Fix NatF. 나의 이해는 즉 Fix NatF이다 N (자연수의 집합), 즉 Nat = Zero | Succ Nat.

Fx정확히 어떻게 정의됩니까? 이 올바른지?

Fx ZeroF = Zero
Fx (SuccF ZeroF) = Succ (Fx ZeroF) = Succ (Zero)

그렇다면 왜 이것은 쌍 [0, succ]에 의해 평가 된 초기 대수 1 + N-> N 과 같지 않습니까?

---

원본 게시물

자연수의 경우 펑터 F (U) = 1 + U 와 단위 가 0이 되고 n 이 succ (n) = n + 1이 되는 초기 대수 F (U)-> U 가 있다는 것을 알고 있습니다 . 함수 평가 다른 대수 H 의 catamorphism의 CATA는 것이다 CATA (N) = H ^N (단위) .

따라서 functor를 다음 data NatF a = ZeroF | SuccF a과 같이 쓸 수 있으며 고정 소수점입니다.data Nat = Zero | Succ Nat

그럼 우리가 정의 Fx :: NatF (Fix NatF) -> Fix NatF하거나 말할 수있을 것 같아요Fix NatF = Fx (NatF (Fix NatF))

String이와 같은 캐리어 유형으로 다른 대수를 정의 하면

h :: NatF String -> String
h ZeroF  = "0"
h (SuccF x) = x ++ " + 1"

다음 cata h = h . fmap (cata h) . unFix과 같이 1과 같은 자연수를 사용할 수 있다고 생각 합니다.

(h . fmap (cata h) . unFix) Fx(SuccF Fx(ZeroF)) =
(h . fmap (cata h)) (SuccF Fx(ZeroF)) =
h (SuccF (cata h)(Fx(ZeroF))) =
h(SuccF h(ZeroF)) =
h (SuccF "0") =
"0 + 1"

그러나 이것은 공식 cata (n) = h ⁿ (unit) 아닌 것 같습니다 . 이 모든 것에서 내 실수는 어디에 있습니까?

Answer 1

나는 당신의 혼란이 cata (n) = h ⁿ (unit) 과 관련이 있다고 생각합니다 . 이것은 사실이 아닙니다-당신은 하나의 오류가 있습니다. 특히, 초기 대수에 대한 정의 교환 다이어그램을 고려하십시오 nat :: 1 + Nat -> Nat.

          nat
1 + Nat  --->   Nat

  |              |
  | F(cata)      |  cata
  V              V
          h
1 + A    --->    A

이것은 우리가하는 일을 더 명확하게하기 위해 인자에 대한 Haskell과 같은 "유형 주석"과 함께 다음을 제공합니다.

cata(0 :: Nat)
-- by definition of nat(unit)
= cata(nat(unit :: 1 + Nat) :: Nat)
-- by diagram
= h(F(cata)(unit :: 1 + Nat) :: 1 + A)
-- as F(cata)(unit) = unit
= h(unit :: 1 + A)

그래서, 당신은 실제로 이 (0) = 시간 CATA을 ¹ (단위) . 적절한 일반 공식은 cata (n) = h ^{n + 1} (unit) 입니다.

Answer 2

대수 NatF A -> A는 (동형까지)

• 유형 A
• 상수 z :: A(이것을 "단위"라고 부릅니다)
• 함수 s :: A -> A( "h"라고 부름)

그런 다음 비공식적으로 cata algebra n = s^n(z).

당신의 예에서, h이다

h :: NatF String -> String
h ZeroF  = "0"
h (SuccF x) = x ++ " + 1"

그러나 이것은 단지 형태가 아닌 전체 대수 ( z및 s) s입니다.

h위 의 내용은 다음과 같습니다.

• A = String
• z = "0"
• s x = x ++ " + 1"

그리고 실제로 (비공식 표기법으로) cata h 1 = s^1(z) = s z = "0" ++ " + 1" = "0 + 1".

결론 : h대수와 대수 s"내부"인 형태 를 모두 호출 하는 데 사용하지 마십시오 .