في الجزء الأول من المقالة حول لغة Arend ، درسنا أبسط أنواع الاستقراء والوظائف العودية والفئات والمجموعات.
2. قوائم الفرز في أرند
2.1 قوائم مرتبة في Arend
نحدد نوع القوائم المطلوبة كزوج يتكون من قائمة وإثبات لترتيبها. كما قلنا بالفعل ، في Arend ، يتم تعريف الأزواج التابعة باستخدام الكلمة الرئيسية
\Sigma . نعطي تعريف النوع
Sorted خلال المقارنة مع العينة ، مستوحاة من التعريف الوارد في
المقالة المذكورة بالفعل
حول القوائم المطلوبة. \func SortedList (O : LinearOrder.Dec) => \Sigma (l : List O) (Sorted l) \data Sorted {A : LinearOrder.Dec} (xs : List A) \elim xs | nil => nilSorted | :-: x nil => singletonSorted | :-: x1 (:-: x2 xs) => consSorted ((x1 = x2) || (x1 < x2)) (Sorted (x2 :-: xs))
ملاحظة: تمكن Arend من استنتاج أن النوع
Sorted موجود في الكون
\Prop . حدث هذا لأن الأنماط الثلاثة في تعريف
Sorted هي حصرية بشكل متبادل ،
consSorted ، وكلاهما ينتمي إلى
\Prop .
دعنا نثبت بعض الخصائص الواضحة للتنبؤات
Sorted ، نقول أن ذيل قائمة مرتبة هو في حد ذاته قائمة مرتبة (هذه الخاصية ستكون مفيدة لنا في المستقبل).
\func tail-sorted {O : LinearOrder.Dec} (x : O) (xs : List O) (A : Sorted (x :-: xs)) : Sorted xs \elim xs, A | nil, _ => nilSorted | :-: _ _, consSorted _ xs-sorted => xs-sorted
في
tail-sorted استخدمنا مطابقة الأنماط في قائمة
xs Sorted في نفس الوقت ، بالإضافة إلى ذلك ، استخدمنا
حرف تخطي "_" ، والذي يمكن استبداله بمتغيرات غير مستخدمة.
قد يتساءل المرء عما إذا كان من الممكن في Arend إثبات ملكية القوائم المرتبة ، والمذكورة في القسم 1.3 كمثال على حقيقة لا يمكن إثباتها في Agda دون توضيحات غير مهمة. تذكر أن هذه الخاصية تدعي أنه لإثبات تكافؤ القوائم المرتبة المعرفة من خلال أزواج تابعة ، يكفي للتحقق من مساواة المكونات الأولى للأزواج.
يقال أنه في Arend يمكن الحصول على هذه الخاصية بسهولة نتيجة للبناء
inProp المذكور أعلاه وخاصية
SigmaExt لأزواج
SigmaExt التابعة.
\func sorted-equality {A : LinearOrder.Dec} (l1 l2 : SortedList A) (P : l1.1 = l2.1) : l1 = l2 => SigmaPropExt Sorted l1 l2 P
تم
SigmaPropExt خاصية
SigmaPropExt في الوحدة النمطية
Paths في المكتبة القياسية ، كما تم إثبات وجود العديد من الحقائق الأخرى من الفصل الثاني
من كتاب HoTT ، بما في ذلك
خاصية الامتداد الوظيفي ، هناك.
.n استخدام عامل التشغيل
.n في Arend للوصول إلى جهاز عرض نوع سيجما برقم n (في حالتنا ، نوع سيجما هو
SortedList A ، والتعبير
l1.1 يعني أن المكون الأول من هذا النوع هو تعبير عن النوع
List A ).
2.2 تنفيذ خاصية "كن التقليب"
الآن دعونا نحاول تنفيذ وظيفة فرز القائمة على Arend. بطبيعة الحال ، لا نريد أن يكون لدينا تطبيق بسيط لخوارزمية الفرز ، ولكن تطبيق مع دليل على بعض الخصائص.
بوضوح ، يجب أن تحتوي هذه الخوارزمية على خاصيتين على الأقل:
1. يجب أن تكون نتيجة الخوارزمية قائمة مرتبة.
2. يجب أن تكون القائمة الناتجة من التقليب في القائمة الأصلية.
أولاً ، دعنا نحاول تنفيذ خاصية "كن متقلبًا" للقوائم في Arend. للقيام بذلك ، نقوم بتكييف التعريف المأخوذ
من هنا من أجل Arend.
\truncated \data InsertSpec {A : \Set} (xs : List A) (a : A) (ys : List A) : \Prop \elim xs, ys | xs, :-: y ys => insertedHere (a = y) (xs = ys) | :-: x xs, :-: y ys => insertedThere (x = y) (InsertSpec xs a ys) \truncated \data Perm {A : \Set} (xs ys : List A) : \Prop | permInsert (xs' ys' : List A) (a : A) (Perm xs' ys') (InsertSpec xs' a xs) (InsertSpec ys' a ys) | permTrivial (xs = ys)
يكون
InsertSpec لنا المعنى البديهي التالي: يعني
InsertSpec xs a ys بالضبط أن القائمة
ys هي نتيجة لإدراج العنصر داخل القائمة
xs (في أي موضع). وبالتالي ، يمكن اعتبار
InsertSpec لوظيفة الإدراج.
بوضوح ، يعرّف نوع بيانات
Perm حقًا العلاقة "be permutation":
permInsert مُنشئ
permInsert أن
xs و
ys يسيران بشكل متبادل إذا تم الحصول على
xs و
ys عن طريق إدراج نفس العنصر a في بعض القوائم
xs' و
ys' أطوال أقصر ، والتي هي بالفعل التباديل من بعضها البعض.
بالنسبة لتعريفنا لخاصية "أن يكون التقليب" ، من السهل التحقق من خاصية التناظر.
\func Perm-symmetric {A : \Set} {xs ys : List A} (P : Perm xs ys) : Perm ys xs \elim P | permTrivial xs=ys => permTrivial (inv xs=ys) | permInsert perm-xs'-ys' xs-spec ys-spec => permInsert (Perm-symmetric perm-xs'-ys') ys-spec xs-spec
ملكية النقل العابر هي أيضا راضية عن
Perm ، ولكن التحقق أكثر تعقيدا بكثير. نظرًا لأن هذه الخاصية لا تلعب أي دور في تنفيذ خوارزمية الفرز لدينا ، فإننا نتركها للقارئ كتمرين.
\func Perm-transitive {A : \Set} (xs ys zs : List A) (P1 : Perm xs ys) (P2 : Perm ys zs) : Perm xs zs => {?}
2.3 تغيير في مستويات homotopy بالمقارنة مع العينة
الآن دعونا نحاول تنفيذ وظيفة تدرج عنصرًا في قائمة مرتبة حتى تظل القائمة الناتجة مرتبة. لنبدأ بالتطبيق الساذج التالي.
\func insert {O : LinearOrder.Dec} (xs : List O) (y : O) : List O \elim xs | nil => y :-: nil | :-: x xs' => \case LinearOrder.trichotomy xy \with { | byLeft x=y => x :-: insert xs' y | byRight (byLeft x<y) => x :-: insert xs' y | byRight (byRight y<x) => y :-: x :-: xs' }
يسمح
\case بالتطابق مع عينة من تعبير تعسفي (
\elim يمكن استخدامه فقط في أعلى مستوى من تعريف الوظيفة والمعلمات فقط). إذا طلبت من Arend التحقق من نوع
insert ، فسيتم عرض رسالة الخطأ التالية.
[ERROR] Data type '||' is truncated to the universe \Prop which does not fit in the universe of the eliminator type: List OE In: | byLeft x-leq-y => x :-: insert xs' y While processing: insert
المشكلة هي أنه في فئة
LinearOrder.Dec trichotomy إعطاء تعريف
LinearOrder.Dec باستخدام عامل التشغيل
|| ، والتي ، بدورها ، يتم تحديدها باستخدام الاقتطاع الافتراضي. كما ذكرنا سابقًا ، بالنسبة للأنواع التي تنتمي إلى
\Prop universe ، لا يُسمح بالمطابقة مع نقش في Arend إلا إذا كان نوع التعبير الناتج بحد ذاته تأكيدًا (بالنسبة للوظيفة أعلاه ، تكون النتيجة من النوع
List OE ، وهذا النوع عبارة عن مجموعة).
هل هناك أي طريقة للتغلب على هذه المشكلة؟ أسهل طريقة لحل هذه المشكلة هي تغيير تعريف خاصية ثلاثية الرؤوس. ضع في اعتبارك التعريف التالي لعلم التشريح ثلاثية الأبعاد ، باستخدام النوع غير المقطوع
Or بدلاً من المقطوع
|| :
\func set-trichotomy {A : StrictPoset} (xy : A) => ((x = y) `Or` (x < y)) `Or` (y < x)
هل
trichotomy هذا التعريف في أي شيء عن تعريف
trichotomy الأصلي من خلال
|| ؟ لماذا استخدمنا حتى نوعًا مقطوعًا بشكل مقترح إذا كان يعقد حياتنا ويمنعنا من استخدام مطابقة الأنماط فقط؟
دعنا نحاول الإجابة على السؤال الأول لبداية: بالنسبة لأوامر
StrictPoset الصارمة
StrictPoset الفرق بين
trichotomy StrictPoset هو في الواقع ليس على الإطلاق. لاحظ أن نوع
set-trichotomy عبارة عن بيان. تأتي هذه الحقيقة من حقيقة أن البدائل الثلاثة جميعها في تعريف trichotomy هي حصرية بشكل متبادل بسبب البديهيات من النظام ، ولكل من الأنواع الثلاثة
x = y, x < y, y < x هي في حد ذاتها عبارة عن بيان (
x = y عبارة عن بيان ، لذلك كما هو الحال في تعريف فئة
BaseSet طلبنا أن تكون الوسائط
E عبارة عن مجموعة!).
\func set-trichotomy-isProp {A : StrictPoset} (xy : A) (l1 l2 : set-trichotomy xy): l1 = l2 \elim l1, l2 | inl (inl l1), inl (inl l2) => pmap (\lam z => inl (inl z)) (Path.inProp l1 l2) | inl (inr l1), inl (inr l2) => pmap (\lam z => inl (inr z)) (Path.inProp l1 l2) | inr l1, inr l2 => pmap inr (Path.inProp l1 l2) | inl (inl l1), inl (inr l2) => absurd (lt-eq-false l1 l2) | inl (inr l1), inl (inl l2) => absurd (lt-eq-false l2 l1) | inl (inl l1), inr l2 => absurd (lt-eq-false (inv l1) l2) | inr l1, inl (inl l2) => absurd (lt-eq-false (inv l2) l1) | inl (inr l1), inr l2 => absurd (lt-lt-false l1 l2) | inr l1, inl (inr l2) => absurd (lt-lt-false l2 l1) \where { \func lt-eq-false {A : StrictPoset} {xy : A} (l1 : x = y) (l2 : x < y) : Empty => A.<-irreflexive x (transport (x <) (inv l1) l2) \func lt-lt-false {A : StrictPoset} {xy : A} (l1 : x < y) (l2 : y < x) : Empty => A.<-irreflexive x (A.<-transitive _ _ _ l1 l2) }
في القائمة أعلاه ، فإن
absurd هو تعيين لمبدأ ex falso quodlibet ، والذي تم تعريفه في الوحدة النمطية
المنطق . نظرًا لأن النوع
Empty لا يحتوي على مُنشئين في التعريف (انظر القسم 1.2) ، فليس من الضروري استعراض الحالات في تعريف
absurd :
\func absurd {A : \Type} (x : Empty) : A
بما أننا نعلم الآن أن
set-trichotomy عبارة عن بيان ، يمكننا استنباط خاصية
set-trichotomy من خاصية
trichotomy المعتادة للأوامر القابلة للإلغاء. للقيام بذلك ، يمكننا استخدام البناء
\return \level ، الذي يخبر مؤقت Arend أنه في هذه المرحلة ، فإن المطابقة مع النمط هي عملية مسموح بها (في هذه الحالة ، علينا أن نظهر دليلاً على أن نتيجة دالة
set-trichotomy-property هي عبارة عن بيان).
\func set-trichotomy-property {A : LinearOrder.Dec} (xy : A) : set-trichotomy xy => \case A.trichotomy xy \return \level (set-trichotomy xy) (set-trichotomy-isProp xy) \with { | byLeft x=y => inl (inl x=y) | byRight (byLeft x<y) => inl (inr x<y) | byRight (byRight y<x) => inr (y<x) }
دعنا الآن نحاول الإجابة على السؤال الثاني ، وهو: لماذا ، عند صياغة خصائص الأشياء الرياضية ، من الأفضل استخدام غير عادي ، ولكن اقتُرح بناءً. فكر في هذا الجزء من تعريف الطلبات الخطية غير الخطية (يمكن العثور على التعريفات الكاملة
TotalOrder Lattice TotalOrder في وحدة
LinearOrder ):
\class TotalOrder \extends Lattice { | totality (xy : E) : x <= y || y <= x }
دعونا نحاول الآن أن نتخيل كيف
TotalOrder معنى فئة
TotalOrder إذا كتبنا تعريف حقل الإجمالي من خلال البناء غير المقطوع
Or الإنشاء.
\class BadTotalOrder \extends Lattice { | badTotality (xy : E) : (x <= y) `Or` (y <= x) }
في هذه الحالة ، النوع
(x <= y) `Or` (y <= x) لم يعد بيانًا ، لأن في حالة تساوي قيمتي
x و
y يمكن تنفيذ كلا الخيارين في تعريف
badTotality ، واختيار الفرع الأيسر أو الأيمن في إثبات
badTotality تعسفي تمامًا ويظل وفقًا لتقدير المستخدم - لا يوجد سبب لتفضيل أحد
Or مُنشئ لآخر.
أصبح من الواضح الآن الفرق بين
TotalOrder و
BadTotalOrder . مجموعتان مرتبة
O1 O2 :
TotalOrder دائمًا عندما يكون من الممكن إثبات مساواة المجموعات
O1.E, O2.E والأوامر
O1.<, O2.< معطى عليها (هذه هي الخاصية المطلوبة). من ناحية أخرى ، بالنسبة إلى
O1 O2 :
BadTotalOrder من
BadTotalOrder إثبات مساواة
O1 و
O2 فقط عندما ، مع كل العناصر
x من
E O1.badTotality xx و
O2.badTotality xx .
وبالتالي ، اتضح أن الفئة
BadTotalOrder بحاجة إلى اعتبارها "مجموعة مرتبة
BadTotalOrder خطيًا" ، ولكن "مجموعة مرتبة خطيًا مع اختيار كل عنصر
x الحقل
E للفرع الأيسر أو الأيمن
Or في تطبيق
badTotality xx ".
2.4 فرز الخوارزمية
ننتقل الآن إلى تنفيذ خوارزمية الفرز. دعنا نحاول إصلاح التطبيق الساذج لوظيفة
insert من القسم السابق باستخدام
set-trichotomy-property ثبت (في هذه الحالة ، بسبب الترتيب الأكثر نجاحًا بين قوسين في تعريف
set-trichotomy ، قللنا عدد الحالات التي تم بحثها).
\func insert {O : LinearOrder.Dec} (xs : List O) (y : O) : List O \elim xs | nil => y :-: nil | :-: x xs' => \case set-trichotomy-property xy \with { | inr y<x => y :-: x :-: xs' | inl x<=y => x :-: insert xs' y }
الآن ، دعونا نحاول تنفيذ تماثلية لهذا التعريف للقوائم المطلوبة. سوف نستخدم التصميم
\let … \in ، والذي يسمح لنا بإضافة متغيرات محلية جديدة إلى السياق.
\func insert {O : LinearOrder.Dec} (xs : SortedList O) (y : O) : SortedList O \elim xs | (nil, _) => (y :-: nil, singletonSorted) | (:-: x xs', xs-sorted) => \case set-trichotomy-property xy \with { | inr y<x => (y :-: x :-: xs', consSorted (byRight y<x) xs-sorted) | inl x<=y => \let (result, result-sorted) => insert (xs', tail-sorted x xs' xs-sorted) y \in (x :-: result, {?})
لقد تركنا في الدليل جزءًا غير مكتمل (يشار إليه بالتعبير
{?} ) في المكان الذي تريد أن تظهر فيه القائمة
x :-: result مرتبة. على الرغم من وجود أدلة في سياق ترتيب قائمة
result ، يبقى التحقق من أن
x لا يتجاوز قيمة العنصر الأول في قائمة
result ، والتي ليس من السهل متابعتها من المبنى في السياق (لمشاهدة جميع المباني في الهدف الحالي - هذا ما نسميه الفرع الحالي للحسابات - تحتاج إلى طلب التحقق من النوع من وظيفة
insert ).
اتضح أن
insert أسهل في التنفيذ إذا أثبتنا ترتيب القائمة الناتجة بالتوازي مع دليل مواصفات
insert . تغيير توقيع
insert وكتابة دليل على هذه المواصفات في أبسط الحالات:
\func insert {O : LinearOrder.Dec} (xs : SortedList O) (y : O) : \Sigma (ys : SortedList O) (InsertSpec xs.1 y ys.1) \elim xs | (nil, _) => ((y :-: nil, singletonSorted), insertedHere idp idp) | (:-: x xs', xs-sorted) => \case set-trichotomy-property xy \with { | inr y<x => ((y :-: x :-: xs', consSorted (byRight y<x) xs-sorted), insertedHere idp idp) | inl x<=y => \let ((result, result-sorted), result-spec) => insert (xs', tail-sorted x xs' xs-sorted) y \in ((x :-: result, {?}), insertedThere idp result-spec)
بالنسبة لشريحة واحدة متبقية بدون دليل ، سيقوم Arend بإخراج قيمة السياق التالية:
Expected type: Sorted (x :-: (insert (\this, tail-sorted x \this \this) \this).1.1) Context: result-sorted : Sorted (insert (\this, tail-sorted \this \this \this) \this).1.1 xs-sorted : Sorted (x :-: xs') x : O x<=y : Or (x = y) (O.< xy) O : Dec result : List O y : O xs' : List O result-spec : InsertSpec xs' y (insert (xs', tail-sorted \this xs' \this) y).1.1
لإكمال الاختبار ، سيتعين علينا استخدام
القوة الكاملة لعامل التشغيل
\case : سوف نستخدم مطابقة الأنماط مع 5 متغيرات مختلفة ، وبما أن أنواع بعض المتغيرات قد تعتمد على قيم المتغيرات الأخرى ، فسوف نستخدم مطابقة النمط المعتمدة.
يشير إنشاء النقطتين بشكل صريح إلى أن نوع بعض المتغيرات التي تتم مقارنتها يعتمد على قيم المتغيرات الأخرى (وبالتالي ، في نوع المتغيرات
xs-sorted, result-spec result-sorted في كل من
\case بدلاً من
xs' و
result سوف تطابق العينات المقابلة).
يربط البناء
\return المتغيرات المستخدمة لمطابقة النموذج بنوع النتيجة المتوقعة. بمعنى آخر ، في الهدف الحالي ، في كل بند من الجمل
\case ، سيتم استبدال العينة المقابلة لمتغير
result . بدون هذا البناء ، لن يتم تنفيذ هذا الاستبدال ، ويتزامن هدف جميع الجمل
\case مع الهدف بدلاً من
\case تعبير
\case نفسه.
\func insert {O : LinearOrder.Dec} (xs : SortedList O) (y : O) : \Sigma (ys : SortedList O) (InsertSpec xs.1 y ys.1) \elim xs | (nil, _) => ((y :-: nil, singletonSorted), insertedHere idp idp) | (:-: x xs', xs-sorted) => \case set-trichotomy-property xy \with { | inr y<x => ((y :-: x :-: xs', consSorted (byRight y<x) xs-sorted), insertedHere idp idp) | inl x<=y => \let ((result, result-sorted), result-spec) => insert (xs', tail-sorted x xs' xs-sorted) y \in ((x :-: result, \case result \as result, xs' \as xs', xs-sorted : Sorted (x :-: xs'), result-spec : InsertSpec xs' y result, result-sorted : Sorted result \return Sorted (x :-: result) \with { | nil, _, _, _, _ => singletonSorted | :-: r rs, _, _, insertedHere y=r _, result-sorted => consSorted (transport (\lam z => (x = z) || (x < z)) y=r (Or-to-|| x<=y)) result-sorted | :-: r rs, :-: x' _, consSorted x<=x' _, insertedThere x2=r _, result-sorted => consSorted (transport (\lam z => (x = z) || (x < z)) x2=r x<=x') result-sorted }), insertedThere idp result-spec)
في
consSorted التعليمات البرمجية أعلاه ،
consSorted الوسائط المعقدة الأولى
consSorted في الفقرتين الأخيرتين من مقارنة الأنماط تعليقًا إضافيًا. لفهم ما يعنيه كل من هذين التعبرين ، نستبدلهما بالتعبير
{?} ونطلب من موقت Arend تحديد الأهداف في كلا الموضعين.
يمكنك أن ترى أن هناك و هناك الهدف الحالي هو النوع
(x = r) || O.< xr (x = r) || O.< xr . علاوة على ذلك ، في سياق الهدف الأول ، هناك أماكن
x<=y : Or (x = y) (O.< xy) y=r : y = r
وفي سياق الثانية - المباني
x<=x' : (x = x') || O.< xx' x2=r : x' = r.
واضح بشكل حدسي: لإثبات الهدف الأول ، يكفي استبدال المتغير
r في العبارة الصحيحة
Or (x = y) (O.< xy) بدلاً من المتغير y ، ثم التبديل إلى النوع المقطوع افتراضيًا
|| باستخدام وظيفة
Or-to-|| المعرفة في القسم 1.3 . لإثبات الهدف الثاني ، فقط استبدل بـ
(x = x') || O.< x x' (x = x') || O.< x x' بدلاً من المتغير
x' المتغير
r .
لإضفاء الطابع الرسمي على عملية استبدال التعبير الموصوفة ، توجد وظيفة
transport خاصة في مكتبة Arend القياسية. النظر في توقيعها:
\func transport {A : \Type} (B : A -> \Type) {aa' : A} (p : a = a') (b : B a) : B a'
في حالتنا ، بدلاً من المتغير
A نحتاج إلى استبدال النوع
OE (يمكن حذفه بشكل صريح في حالة تحديد وسائط
transport الأخرى) ، وبدلاً من
B تعبير
\lam (z : O) => (x = z) || (x < z) \lam (z : O) => (x = z) || (x < z) .
لم يعد تطبيق خوارزمية فرز الإدراج جنبًا إلى جنب مع المواصفات يسبب أي صعوبات معينة: من أجل فرز القائمة
x :-: xs' ، سنقوم أولاً بفرز ذيل قائمة
xs' باستخدام مكالمة متكررة
insertSort ، ثم إدراج العنصر
x داخل هذه القائمة مع الحفاظ على الترتيب لـ مساعدة في الوصول إلى وظيفة
insert تنفيذها بالفعل.
\func insertSort {O : LinearOrder.Dec} (xs : List O) : \Sigma (result : SortedList O) (Perm xs result.1) \elim xs | nil => ((nil, nilSorted), permTrivial idp) | :-: x xs' => \let | (ys, perm-xs'-ys) => insertSort xs' | (zs, zs-spec) => insert ys x \in (zs, permInsert perm-xs'-ys (insertedHere idp idp) zs-spec)
حققنا الهدف الأولي ونفذنا فرز القوائم على Arend. يمكن تنزيل رمز Arend بأكمله الوارد في هذه الفقرة في ملف واحد
من هنا .
قد يتساءل المرء كيف يمكن للمرء تغيير تنفيذ وظيفة
insert إذا بدلاً من أوامر
LinearOrder.Dec الصارمة. هل
LinearOrder.Dec أوامر
LinearOrder.Dec غير الصارمة؟ كما نتذكر ، في تعريف الدالة الكلية ، استخدام العملية المقطوعة
|| كان مهمًا جدًا ، أي أن هذا التعريف لا يعادل تعريفًا بدلاً من
|| المستخدمة من قبل
Or .
الإجابة على هذا السؤال هي كالتالي: لا يزال من الممكن إنشاء تماثلي
insert لـ
TotalOrder ، ومع ذلك ، يتعين علينا أن نثبت أن نوع دالة
insert هو عبارة (هذا سيسمح لنا في تعريف
insert بإجراء مقارنة مع العينة وفقًا
totality xy البيان).
بمعنى آخر ، يجب أن نثبت أن هناك قائمة مرتبة واحدة فقط تصل إلى المساواة ، وهي نتيجة لإدراج العنصر
y في القائمة
xs المرتبة. من السهل أن نرى أن هذه حقيقة حقيقية ، لكن دليلها الرسمي لم يعد تافهاً. نترك التحقق من هذه الحقيقة كتمرين للقارئ المهتم.
3. الملاحظات الختامية
في هذه المقدمة ، تعرفنا على التركيبات الرئيسية للغة Arend ، وتعلمنا أيضًا استخدام آلية الفصل. تمكنا من تنفيذ أبسط الخوارزمية جنبا إلى جنب مع إثبات مواصفاتها. وبالتالي ، فقد أظهرنا أن Arend مناسب تمامًا لحل المشكلات "اليومية" ، مثل التحقق من البرنامج على سبيل المثال.
لقد ذكرنا بعيدًا عن كل ميزات وميزات Arend. على سبيل المثال ، لم نذكر شيئًا تقريبًا عن
الأنواع ذات الشروط التي تسمح لك "بإلصاق" مُنشئات
الأنواع المختلفة مع بعض قيم المعلمات الخاصة لهذه المنشئات. على سبيل المثال ، يتم إعطاء تطبيق نوع صحيح في Arend باستخدام أنواع ذات شروط كما يلي:
\data Int | pos Nat | neg Nat \with { zero => pos zero }
يشير هذا التعريف إلى أن الأعداد الصحيحة تتكون من نسختين من نوع الأرقام الطبيعية ، حيث يتم تحديد الأصفار "الإيجابية" و "السلبية". يعد هذا التعريف أكثر ملاءمة من التعريف الموجود في مكتبة Coq القياسية ، حيث يجب تبديل "النسخة السالبة" من الأرقام الطبيعية بواسطة واحد حتى لا تتقاطع هذه النسخ (يكون أكثر ملاءمة عندما تدوين
neg 1 يعني الرقم -1 ، وليس -2) .
لم نقول شيئًا عن الخوارزمية لاشتقاق مستويات التقييم والتماثل في الفصول الدراسية ومثيلاتها. بالكاد ذكرنا نوع الفاصل
I ، على الرغم من أنه يلعب دورًا رئيسيًا في نظرية الأنواع ذات الفواصل الزمنية ، والتي هي الأساس المنطقي لـ Arend. لفهم مدى أهمية هذا النوع ، يكفي أن نذكر أنه في Arend ، يتم تعريف المساواة من خلال مفهوم الفاصل الزمني. , , , (.. ).
:
,
HoTT JetBrains Research.