بين قوسين بعد كتابة البيئة

Question

لقد قرأت عن System F Omega مؤخرًا، وما زلت أتعثر في بناء قواعد الكتابة التي لا أستطيع العثور على تفسير لها: Γ(x) = k.على سبيل المثال، في مقدمة قصيرة للأنظمة F و F Omega:

Γ(a) = k
--------
Γ ⊢ a : k

أرى نفس البناء في الاستبدال الوراثي للنظام الطبقي F.أنا أفهم الجزء السفلي بشكل جيد.سوف يقرأ شيئا مثل:"في سياق Γ, a لديه نوع k".لم أتمكن من العثور على شرح للجزء العلوي، والمصادر التي أشرت إليها تفترض الإلمام بهذا البناء.إذا كان علي أن أخمن، أظن أن ذلك يعني شيئًا مثل "في السياق a, ، تشغيل خوارزمية التحقق من النوع a يعطيك النوع k كنتيجة".هل هذا دقيق؟ما هي الموارد عبر الإنترنت التي تصف هذا البناء؟

Answer 1

$\غاما$ هنا تدوين مثقل.معنى التعبير $\جاما(x) = au$ فوق خط الاستدلال هنا مذكور تحت "اكتب القواعد." قسم من مقدمة قصيرة للأنظمة F و F Omega في الصفحة 5.في هذا الإعداد، $\غاما$ هي دالة محددة حثيًا ترسل المتغيرات (في $\غاما$ تعتبر سياقا، أي.قائمة المتغيرات) لأنواعها.

قد تكون الطريقة التوضيحية والنحوية الأكثر لكتابة القاعدة التي تقدمها هي: $\frac{}{\Gamma,\ x : au\ \vdash س :\تاو}$, ، أين $\غاما$ يتراوح بحرية على السياقات.لاحظ أن ترتيب المتغيرات في السياق هنا لا يهم، لذا فإن هذه القاعدة تسمح لنا بإسقاط أي متغير في السياق كمصطلح.

Answer 2

للإضافة إلى إجابة varcor:

السياق هو مجرد وظيفة ترسل (بعض) المتغيرات إلى أنواعها.

لذلك القاعدة تقول:"لو $\غاما$ يعين النوع $\تاو$ إلى متغير $x$, ، ثم يمكننا أن نستنتج $\جاما \vdash س :\تاو$."