كيفية تعلم AGDA

Question

أحاول تعلم AGDA.ومع ذلك، حصلت على مشكلة.جميع البرامج التعليمية التي عثرت عليها في Agda Wiki معقدة للغاية بالنسبة لي وتغطي جوانب مختلفة من البرمجة.بعد القراءة الموازية ل 3 دروس على AGDA، تمكنت من كتابة البراهين البسيطة ولكن ما زلت لا أملك معرفة كافية لاستخدامها لصحة خوارزمية الكلمة الحقيقية.

هل يمكن أن تنصحني بأي برامج تعليمية حول هذا الموضوع؟شيء مشابه لتعلم نفسك هاسكل ولكن بالنسبة لأجدة.

Answer 1

عندما بدأت في تعلم AGDA منذ حوالي عام، أعتقد أنني جربت جميع البرامج التعليمية المتاحة وعلنت كل منها شيئا جديدا.

يجب أن تعطي COQ جربا، لأنه يحتوي على قاعدة مستخدم أكبر وهناك كتابان لطيفان له:

1. li> coq'art - مؤرخة قليلا، ولكن المبتدئين ودية
2. li> برمجة معتمدة مع الأنواع التابعة

   href="http://www.cis.upenn.edu/~bcpierce/sf/"> مؤسسات البرامج هي أيضا لطيفة جدا.

   الشيء اللطيف هو أن نظريات Agda و Coq تستند إليها متشابهة إلى حد ما، لذلك يمكن ترجمة العديد من الأمثلة من واحدة إلى أخرى. نظرية نوع Martin-Löf's Type هي مقدمة لطيفة وقابلة للقراءة في نظرية النوع التابعة ، يمكن أن تطهير بعض الأشياء بالنسبة لك.

   سيساعد على معرفة ماذا تقصد ب "خوارزميات العالم الحقيقي". يتم وصف العديد من التطورات على سبيل المثال في الأوراق التي ذكر Agda .

Answer 2

أعطى كونور ماكبرايد سلسلة رائعة من المحاضرات العام الماضي على البرمجة المكتوبة بصدق باستخدامagda.إنه مكان جيد للذهاب إذا كنت تريد استراحة من التبول من خلال دروس TERSE حول هذا الموضوع.أعتقد أن هناك أيضا تمارين مصاحبة.