Cách tìm hiểu agda

Question

Tôi đang cố gắng tìm hiểu agda. Tuy nhiên, tôi có một vấn đề. Tất cả các hướng dẫn mà tôi tìm thấy trên wiki agda là quá phức tạp đối với tôi và bao gồm các khía cạnh khác nhau của lập trình. Sau khi đọc song song 3 hướng dẫn trên agda tôi đã có thể viết các chứng minh đơn giản nhưng tôi vẫn không có đủ kiến ​​thức để sử dụng nó cho đúng thuật toán từ đúng.

Bạn có thể giới thiệu cho tôi bất kỳ hướng dẫn nào về chủ đề này không? Một cái gì đó tương tự như Tìm hiểu cho mình một Haskell nhưng đối với Agda.

Answer 1

Khi tôi bắt đầu học Agda khoảng một năm trước, tôi nghĩ rằng tôi đã thử tất cả các hướng dẫn có sẵn và mỗi người đã dạy tôi điều gì đó mới mẻ.

Bạn có lẽ nên cho Coq thử, bởi vì nó có một cơ sở người dùng lớn hơn và có hai cuốn sách tốt đẹp sẵn có cho nó:

1. Coq'Art - hơi ngày, nhưng người mới bắt đầu thân thiện
2. Certified Programming with Dependent Types

Software Foundations cũng rất đẹp.

Điều thú vị là các lý thuyết Agda và Coq được dựa trên có phần tương tự nhau, vì vậy nhiều ví dụ có thể được dịch từ một đến khác. Programming in Martin-Löf's Type Theory là một giới thiệu thực sự tốt đẹp và dễ đọc đối với lý thuyết loại phụ thuộc, nó có thể xóa một số điều cho bạn.

Nó sẽ giúp bạn hiểu ý nghĩa của "thuật toán thực tế". Nhiều ví dụ phát triển được mô tả trong papers which mention Agda.

Answer 2

Conor McBride tặng a great series of lectures năm ngoái về lập trình được đánh máy phụ thuộc bằng Agda. Đó là một nơi tốt để đi nếu bạn muốn có một break từ rót qua hướng dẫn terse về chủ đề này. Tôi tin rằng cũng có những bài tập đi kèm.