Last có phải là một monoid miễn phí?

Sep 17 2020

Các monoids tự do thường được coi là "danh sách các monoids". Tuy nhiên, tôi quan tâm đến các cấu trúc khả thi khác có thể cung cấp cho chúng ta các monoids miễn phí .

Trước hết, chúng ta hãy xem xét định nghĩa về các monoids tự do . Tôi chưa bao giờ hiểu rõ làm thế nào để có thể định nghĩa một monoid tự do là một cấu trúc tuân theo luật monoid và không có gì khác. Làm thế nào để chúng tôi chứng minh rằng một cái gì đó không tuân theo các quy tắc nhưng đã nêu ở trên? Hay đây chỉ là trực giác?

Dù sao đi nữa, chúng ta sẽ nói chuyện về những kẻ vui nhộn Nếu một số monoid miễn phí , chúng tôi đã nhận nó với một functor miễn phí . Rõ ràng là một danh sách khá hữu ích ở đây:

free :: Set -> Mon
free a = ([a], (++), [])

Tuy nhiên, một người có thể nghĩ ra một số người khác. Ví dụ, đây là một trong Lastsố Data.Monoid:

freeLast :: Set -> Mon
freeLast a = (Last a, (<>) :: Last a -> Last a -> Last a, Last Nothing)

Vì vậy, liệu functor này có tạo ra Lastmột monoid miễn phí ? Nói một cách tổng quát hơn, nếu có một trường hợp tuân thủ pháp luật Monoid (T a), liệu có phải là Tmột đơn vị miễn phí không?

Trả lời

11 BartoszMilewski Sep 17 2020 at 09:56

Đây là một cách để hiểu về monoid miễn phí: Nếu ai đó cung cấp cho bạn một giá trị, bạn có thể suy ra bao nhiêu về cách nó được tạo ra? Hãy xem xét một đơn thức cộng của các số tự nhiên. Tôi cho bạn điểm 7 và hỏi bạn làm thế nào tôi có được nó. Tôi có thể đã thêm 4 + 3, hoặc 3 + 4, hoặc 2 + 5, v.v. Có rất nhiều khả năng. Thông tin này đã bị mất. Mặt khác, nếu tôi cung cấp cho bạn một danh sách [4, 3], bạn biết rằng nó được tạo ra từ các đĩa đơn [4]và [3]. Ngoại trừ việc có thể có một đơn vị []tham gia. Có lẽ nó đã được [4]<>[3]<>[]hoặc [4]<>[]<>[]<>[3]. Nhưng chắc chắn là không [3]<>[4].

Với danh sách dài hơn [1, 2, 3], bạn có các tùy chọn bổ sung ([1]<>[2]) <> [3], hoặc [1] <> ([2]<>[3])cộng với tất cả các phần chèn có thể có của danh sách trống. Vì vậy, thông tin bạn mất tuân theo luật đơn vị và tính liên kết, chứ không có gì khác . Giá trị monoid miễn phí ghi nhớ cách nó được tạo ra, luật đơn vị mô đun và tính liên kết.

4 lsmor Sep 17 2020 at 17:50

Ví dụ, hãy lấy số nguyên không âm, tức là 0,1,2,.... Chúng ta có thể tạo ra bao nhiêu đơn chất?

Định nghĩa mempty = 0và (<>) = (+). Bạn có thể dễ dàng chứng minh rằng đây là một chiếc monoid.

Định nghĩa mempty = 1và (<>) = (*). Một lần nữa, Đây là một monoid (Chứng minh nó, nó rất dễ dàng)

Hai đơn thức được xác định ở trên, được gọi là đơn thức cộng và đơn bội trên Số tự nhiên. Chúng khác nhau về cấu trúc, ví dụ, phần tử 0trong đơn thức nhân, hoạt động hoàn toàn khác với bất kỳ phần tử nào khác trong đơn thức cộng, do đó có một cái gì đó bên trong Số tự nhiên, điều đó làm cho đơn thức này khác biệt (giữ khẳng định này cho đến đoạn tiếp theo ).

Có một monoid thứ ba mà chúng ta có thể tạo, hãy gọi nó là monoid nối .

Định nghĩa mempty = no-actionvà (<>) = glue one integer beside the other.

Ví dụ, 3 <> mempty = 3và 3 <> 2 = 32. Lưu ý rằng thực tế là các phần tử, là số tự nhiên không liên quan ở đây. Nếu thay vì tự nhiên, chúng ta hãy rationals hay bất cứ những biểu tượng mà bạn thích, các monoid sẽ được chính xác những điều tương tự. (* Đọc chú thích cuối trang) Do đó, không có gì bên trong để các thiết lập cơ bản mà làm cho sự khác nhau monoid cho người khác là . Đó là lý do tại sao, monoid là miễn phí vì nó không phụ thuộc vào các quy tắc số học của Naturals, cũng như bất kỳ quy tắc nào khác ngoài các monoid.

Và đây là cách duy nhất để xây dựng monoid một cách tự do, không phụ thuộc vào các quy tắc bên trong của tập hợp bên dưới. Tất nhiên, nối được thể hiện dưới dạng danh sách trong haskell.

Lưu ý: Điều quan trọng duy nhất là chúng có cùng số phần tử. Ví dụ, monoid miễn phí với 3 yếu tố a, bvà csẽ là bất kỳ nối độc đoán của ba, nhưng bạn có thể chọn những gì bao giờ biểu tượng: 1, 2, 3hay α, β, γ... và monoid sẽ là điều rất giống nhau

3 amalloy Sep 17 2020 at 04:18

Đây là một luật khác Lastthỏa mãn:

forall (t :: Type) (x, y :: t).
  Last (Just x) <> Last (Just y) === Last (Just y)

Vì nó thỏa mãn một định luật khác, nó không phải là Monoid miễn phí.

3 Li-yaoXia Sep 17 2020 at 10:28

Trước hết, chúng ta hãy xem xét định nghĩa về các monoids tự do. Tôi chưa bao giờ hiểu rõ làm thế nào để có thể định nghĩa một monoid tự do là một cấu trúc tuân theo luật monoid và không có gì khác. Làm thế nào để chúng tôi chứng minh rằng một cái gì đó không tuân theo các quy tắc nhưng đã nêu ở trên? Hay đây chỉ là trực giác?

Hãy để tôi minh họa mục đích của monoids miễn phí.

Nếu tôi nói với bạn có một monoid, với một số yếu tố a, b, c, những gì có thể giúp bạn suy ra từ đó?

Chúng tôi có thể tìm thêm các yếu tố của monoid rằng bằng cách viết biểu thức liên quan đến máy phát điện a , b, cvà các hoạt động monoid (+)và 0(aka. (<>)Và mempty). (xem Định nghĩa 1, trong nửa sau của câu trả lời này.)
Chúng ta có thể sử dụng các định luật đơn thức để chứng minh rằng một số biểu thức biểu thị cùng một nguyên tố: chúng ta có thể chứng minh các đẳng thức chẳng hạn như ((a + 0) + b) = (a + b). (Định nghĩa 2.) Trong thực tế, phương trình chúng ta có thể chứng minh với chỉ kiến thức mà là phương trình mà giữ trong bất kỳ monoid, đối với bất kỳ giá trị a, b, c. (Định lý 1.)

Điều gì về các phương trình chúng ta không thể chứng minh chỉ từ các định luật đơn nguyên? Ví dụ, chúng tôi không thể chứng minh (a + b) = (b + a). Nhưng chúng ta cũng không thể chứng minh sự phủ định của nó (a + b) /= (b + a), nếu chúng ta chỉ biết các luật đơn nguyên. Điều đó nghĩa là gì? Nó chỉ ra rằng phương trình đó đúng trong một số đơn chất (ví dụ, đơn chất giao hoán), nhưng không đúng ở những đơn vị khác: ví dụ, chọn một đơn nguyên ở x + y = ygần như tất cả xvà y(đây là Lastđơn nguyên trong Haskell), nếu chúng ta chọn khác biệt avà bsau đó (a + b) /= (b + a).

Nhưng đó chỉ là một ví dụ. Nói chung chúng ta có thể nói gì về các phương trình mà chúng ta không thể chứng minh được chỉ từ các định luật đơn nguyên? Các monoid cung cấp miễn phí một câu trả lời dứt khoát, trên thực tế, một phản ví dụ phổ biến: phương trình không thể chứng minh là sai trong monoid miễn phí (được tạo ra bởi a, b, c). Nói cách khác, chúng ta có thể chứng minh một phương trình e = fchỉ sử dụng các định luật đơn nguyên nếu và chỉ khi nó đúng trong đơn thức tự do (nhấn mạnh vào "nếu"). (Định lý 2.) Điều này tương ứng với trực giác rằng đơn nguyên tự do "chỉ tuân theo các định luật đơn nguyên và không có gì khác".

Vậy, functor này có làm cho Last trở thành monoid miễn phí không? Nói một cách tổng quát hơn, nếu có một trường hợp tuân thủ pháp luật cho Monoid (T a), thì T có phải là monoid miễn phí không?

Các Lastmonoid là không được tự do bởi vì nó làm cho nhiều phương trình đúng hơn những gì bạn thực sự có thể chứng minh hoàn toàn so với luật monoid. Xem câu trả lời khác :

forall (t :: Type) (x, y :: t).
  Last (Just x) <> Last (Just y) === Last (Just y)

Đây là một bản phác thảo về cách chính thức hóa những điều trên.

Định nghĩa 1. Tập hợp các biểu thức monoidal tạo ra bởi (một số biểu tượng nguyên tử) A, B, Cđược xác định bởi ngữ pháp:

e ::=
  | A | B | C   -- generators
  | e + e       -- binary operation (<>)
  | 0           -- identity (mempty)

Đưa ra bất kỳ "monoid phù hợp", có nghĩa là phải nói, một monoid (M, (+), 0)với một số yếu tố được lựa chọn a, b, ctrong M(mà không phải là riêng biệt), một biểu thức ebiểu thị một yếu tố eval etrong M.

Định nghĩa 2. Một phương trình là một cặp biểu thức, viết e ~ f. Tập phương trình có thể cho là tập phương trình nhỏ nhất ("nhỏ nhất" khi được sắp xếp theo thứ tự bao gồm) thỏa mãn các điều kiện sau:

Nó bao gồm các luật monoid: (e + 0) ~ e, (0 + e) ~ e, ((e + f) + g) ~ (e + (f + g))là chứng minh.
Nó là một quan hệ tương đương (xem một tập hợp các bộ giá trị như một quan hệ): ví dụ, đối với tính phản xạ, e ~ elà có thể chứng minh được.
Đó là một mối quan hệ tương đẳng: nếu e ~ flà chứng minh sau đó (g + e) ~ (g + f)và (e + g) ~ (f + g)được chứng minh.

(Ý tưởng của định nghĩa đó là khẳng định " e ~ fcó thể chứng minh được" đúng nếu và chỉ khi nó có thể được suy ra bằng cách "áp dụng" các quy tắc đó. "Tập hợp nhỏ nhất" là một phương pháp thông thường để chính thức hóa điều đó.)

Định nghĩa về "phương trình có thể chứng minh" có vẻ tùy tiện. Đó có phải là những quy tắc đúng để xác định "khả năng dự phòng" không? Tại sao lại nói riêng ba quy tắc này? Đáng chú ý, quy tắc đồng dư có thể không rõ ràng trong nỗ lực đầu tiên đưa ra định nghĩa như vậy. Đây là điểm của các định lý sau đây, tính đúng đắn và đầy đủ. Thêm một quy tắc (không thừa), và chúng ta sẽ mất đi tính hợp lý. Xóa một quy tắc và chúng tôi mất tính hoàn chỉnh.

Định lý 1. (Độ âm thanh) Nếu e ~ fcó thể chứng minh được thì eval e = eval ftrong bất kỳ "đơn âm phù hợp" nào M.

Định lý 2. (Đầy đủ) Nếu e ~ fkhông phải là chứng minh, sau đó denotations của họ khác nhau về F, eval e /= eval fnơi Flà monoid tự do sinh ra bởi A, B, C.

(Tính rõ ràng dễ chứng minh hơn tính hoàn chỉnh. Bài tập cho người đọc.)

Định lý đầy đủ này là một đặc điểm của đơn thức tự do: bất kỳ đơn thức nào khác Fgiữ cho phát biểu của định lý đúng là đẳng cấu với đơn nguyên tự do (về mặt kỹ thuật, điều này đòi hỏi cả tính hoàn chỉnh và giả định rằng hàm ký hiệu eval : Expr -> Mlà hàm phụ ). Đó là lý do tại sao chúng ta có thể nói "đơn miễn phí" thay vì "đơn danh sách"; thực tiễn đó là chính xác nhất trong các ngữ cảnh mà việc biểu diễn không quan trọng ("tối đa là đẳng cấu").

Trên thực tế, tính đầy đủ là nhỏ nếu bạn định nghĩa "đơn thức tự do" là thương số của biểu thức đơn nguyên bằng quan hệ tương đương " _ ~ _có thể chứng minh được". Công việc khó khăn thực sự nằm ở một bằng chứng riêng biệt, rằng monoid này là đồng phân với monoid của danh sách.