"إيجابي تمامًا" في AGDA

Question

أحاول تشفير بعض الدلالات الدلالية إلى AGDA استنادًا إلى برنامج كتبته في Haskell.

data Value = FunVal (Value -> Value)
           | PriVal Int
           | ConVal Id [Value]
           | Error  String

في AGDA ، ستكون الترجمة المباشرة ؛

data Value : Set where
    FunVal : (Value -> Value) -> Value
    PriVal : ℕ -> Value
    ConVal : String -> List Value -> Value
    Error  : String -> Value

لكني أحصل على خطأ فيما يتعلق بـ funval لأن ؛

القيمة ليست إيجابية تمامًا ، لأنها تحدث على يسار السهم في نوع Funval المنشئ في تعريف القيمة.

ماذا يعني هذا؟ هل يمكنني تشفير هذا في AGDA؟ هل سأذهب حول هذا الأمر بطريقة خاطئة؟

شكرًا.

Answer 1

هواس لا يعمل في أجدا ، بسبب هذا:

apply : Value -> Value -> Value
apply (FunVal f) x = f x
apply _ x = Error "Applying non-function"

w : Value
w = FunVal (\x -> apply x x)

الآن ، لاحظ أن التقييم apply w w يعطيك apply w w عاد ثانية. المصطلح apply w w ليس له شكل طبيعي ، وهو لا في AGDA. باستخدام هذه الفكرة والنوع:

data P : Set where
    MkP : (P -> Set) -> P

يمكننا اشتقاق تناقض.

تتمثل إحدى طرق هذه المفارقات فقط في السماح بأنواع العودية الإيجابية تمامًا ، وهو ما تختاره AGDA و COQ. هذا يعني أنه إذا أعلن:

data X : Set where
    MkX : F X -> X

الذي - التي F يجب أن يكون functor إيجابي للغاية ، مما يعني ذلك X قد لا تحدث على يسار أي سهم. لذلك هذه الأنواع إيجابية تمامًا في X:

X * X
Nat -> X
X * (Nat -> X)

لكن هذه ليست:

X -> Bool
(X -> Nat) -> Nat  -- this one is "positive", but not strictly
(X * Nat) -> X

باختصار ، لا ، لا يمكنك تمثيل نوع البيانات في AGDA. يمكنك استخدام ترميز De Bruijn للحصول على نوع مصطلح يمكنك العمل معه ، ولكن عادةً ما تحتاج وظيفة التقييم ليكون المجموع. هنا مثال بسبب gallais الذي يستخدم نوع التحيز coidection لإنجاز هذا.