المنطق الخطي

المنطق الخطي هو منطق بنيوي فرعي اقترحه عالم المنطق الفرنسي جان إيف جيرار كتحسين للمنطق الكلاسيكي والحدسي ، جامعًا بين ثنائيات الأول والعديد من الخصائص البنائية للثاني. ^{[ 1 ]} على الرغم من دراسة هذا المنطق لذاته، إلا أن أفكاره كانت مؤثرة بشكل أوسع في مجالات مثل لغات البرمجة ، ودلالات الألعاب ، وفيزياء الكم (لأن المنطق الخطي يُمكن اعتباره منطق نظرية المعلومات الكمومية )، ^{[ 2 ]} بالإضافة إلى اللغويات ، ^{[ 3 ]} لا سيما بسبب تركيزه على محدودية الموارد، والثنائية، والتفاعل.

يُتيح المنطق الخطي إمكانية تقديمه وتفسيره وتفسيره بطرقٍ مُتعددة. من الناحية البرهانية ، ينبثق من تحليل حساب التتابعات الكلاسيكي ، حيث تُضبط استخدامات قواعد الانكماش والتضعيف ( القواعد البنيوية ) بدقة. عمليًا، يعني هذا أن الاستدلال المنطقي لم يعد مجرد مجموعة متنامية من "الحقائق" الثابتة، بل أصبح أيضًا وسيلةً للتعامل مع موارد لا يُمكن تكرارها أو التخلص منها بسهولة. من منظور النماذج الدلالية البسيطة ، يُمكن اعتبار المنطق الخطي بمثابة تحسين لتفسير المنطق الحدسي من خلال استبدال الفئات الديكارتية (المغلقة) بفئات أحادية متناظرة (مغلقة) ، أو تفسير المنطق الكلاسيكي من خلال استبدال الجبر البولياني بجبر C* .

تتبع هذه المقالة ترميز جيرارد. وللقراء الملمين بالترميزات المختلفة، يقارن الجدول التالي، الذي جمعه باولي عام 2002، ^{[ 4 ]} الترميزات المستخدمة في الروابط والثوابت المنطقية الخطية عبر مصادر متعددة.

جيرارد 1987 [ 5 ]	ترويلسترا 1992 [ 6 ]	ريستال 2000 [ 7 ]	باولي 2002 [ 4 ]
${\displaystyle \bot }$	${\displaystyle \sim }$	${\displaystyle \sim }$	${\displaystyle \neg }$
${\displaystyle \otimes }$	${\displaystyle \star }$	${\displaystyle \circ }$	${\displaystyle \otimes }$
⅋	${\displaystyle +}$	${\displaystyle +}$	${\displaystyle \oplus }$
${\displaystyle \&}$	${\displaystyle \sqcap }$	${\displaystyle \wedge }$	${\displaystyle \wedge }$
${\displaystyle \oplus }$	${\displaystyle \sqcup }$	${\displaystyle \vee }$	${\displaystyle \vee }$
${\displaystyle \multimap }$	${\displaystyle \multimap }$	${\displaystyle \rightarrow }$	${\displaystyle \rightarrow }$
${\displaystyle$ !}	${\displaystyle$ !}	${\displaystyle$ !}	${\displaystyle$ !}
${\displaystyle$ ؟}	${\displaystyle$ ؟}	${\displaystyle$ ؟}	${\displaystyle$ ؟}
${\displaystyle \mathbf {1} }$	${\displaystyle \mathbf {1} }$	${\displaystyle \mathbf {1} }$	${\displaystyle \mathbf {1} }$
${\displaystyle \bot }$	${\displaystyle \mathbf {0} }$	${\displaystyle \mathbf {0} }$	${\displaystyle \mathbf {0} }$
${\displaystyle \top }$	${\displaystyle \top }$	${\displaystyle \top }$	${\displaystyle \top }$
${\displaystyle \mathbf {0} }$	${\displaystyle \bot }$	${\displaystyle \bot }$	${\displaystyle \bot }$

إحدى طرق تعريف المنطق الخطي هي اعتباره حسابًا للمتتاليات . نستخدم الحرفين Γ و Δ للتنقل بين قوائم محدودة من القضايا A1 ، ...، An _، والتي تُسمى أيضًا سياقات . تضع المتتالية سياقًا على يسار ويمين البوابة الدوارة ، ويرمز لها بالحرف Γ _.${\displaystyle \vdash }$Δ . بشكل بديهي، تؤكد المتتالية أن اقتران Γ يستلزم فصل Δ (مع أننا نقصد الاقتران والفصل "الضربي"، كما هو موضح أدناه). يصف جيرارد المنطق الخطي الكلاسيكي باستخدام متتاليات أحادية الجانب فقط (حيث يكون السياق الأيسر فارغًا)، ونتبع هنا هذا العرض الأكثر اقتصادًا. هذا ممكن لأن أي مقدمات على يسار بوابة الدوران يمكن دائمًا نقلها إلى الجانب الآخر وتحويلها إلى ثنائية.

نقدم الآن قواعد الاستدلال التي تصف كيفية بناء براهين المتتاليات. ^{[ 8 ]}

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

${\displaystyle \vdash }$Γ، A1 ، A2 ، Δ

${\displaystyle \vdash }$Γ، A 2 ، A 1 ، Δ

لاحظ أننا لا نضيف القواعد الهيكلية للتضعيف والانكماش، لأننا نهتم بغياب القضايا في التسلسل، وعدد النسخ الموجودة.

ثم نضيف التسلسلات الأولية والقطع :

${\displaystyle \vdash }$أ ، أ ⊥

${\displaystyle \vdash }$Γ، أ ${\displaystyle \vdash }$A ⊥ , Δ ${\displaystyle \vdash }$Γ، Δ

يمكن اعتبار قاعدة القطع طريقةً لتكوين البراهين، وتُستخدم المتتاليات الأولية كوحداتٍ لهذا التكوين. وبمعنى ما، تُعدّ هذه القواعد زائدةً عن الحاجة: فمع تقديمنا لقواعد إضافية لبناء البراهين لاحقًا، سنحصل على خاصية إمكانية اشتقاق أي متتالية أولية من متتاليات أولية ذرية، وأنه كلما أمكن إثبات متتالية ما، يُمكن تقديم برهانٍ خالٍ من القطع. في نهاية المطاف، تكمن خاصية الشكل المتعارف عليه هذه (والتي يُمكن تقسيمها إلى اكتمال المتتاليات الأولية الذرية ونظرية حذف القطع ، مما يُؤدي إلى مفهوم البرهان التحليلي ) وراء تطبيقات المنطق الخطي في علوم الحاسوب، إذ تُتيح استخدام هذا المنطق في البحث عن البراهين وكحساب لامدا مُراعي للموارد .

الآن، نشرح الروابط المنطقية من خلال وضع قواعد منطقية . عادةً في حساب المتتابعات، تُذكر "قواعد يمين" و"قواعد يسار" لكل رابط منطقي، ما يصف نمطين من الاستدلال حول القضايا التي تتضمن ذلك الرابط (مثل التحقق والتفنيد). في عرض أحادي الجانب، يُستخدم النفي: إذ تؤدي قواعد اليمين لرابط منطقي (مثلاً ⅋) دور قواعد اليسار لنظيره (⊗). لذا، نتوقع وجود نوع من "التوافق" بين قواعد الرابط المنطقي وقواعد نظيره.

الضرب

قواعد الربط المضاعف (⊗) والفصل (⅋):

${\displaystyle \vdash }$Γ، أ ${\displaystyle \vdash }$دلتا، ب ${\displaystyle \vdash }$Γ، Δ، A ⊗ B

${\displaystyle \vdash }$Γ، A ، B ${\displaystyle \vdash }$Γ، A ⅋ B

ولوحداتهم:

${\displaystyle \vdash }$1

${\displaystyle \vdash }$Γ ${\displaystyle \vdash }$Γ, ⊥

لاحظ أن قواعد الاقتران والفصل المضاعف مقبولة للاقتران والفصل البسيطين في ظل تفسير كلاسيكي (أي أنها قواعد مقبولة في LK ).

المواد المضافة

قواعد الربط الجمعي (&) والفصل (⊕):

${\displaystyle \vdash }$Γ، أ ${\displaystyle \vdash }$Γ، B ${\displaystyle \vdash }$Γ، A و B

${\displaystyle \vdash }$Γ، أ ${\displaystyle \vdash }$Γ، A ⊕ B

${\displaystyle \vdash }$Γ، B ${\displaystyle \vdash }$Γ، A ⊕ B

ولوحداتهم:

${\displaystyle \vdash }$Γ, ⊤

(لا توجد قاعدة للصفر )

لاحظ أن قواعد الربط والفصل الجمعي مقبولة مرة أخرى وفقًا للتفسير الكلاسيكي. ولكن الآن يمكننا شرح أساس التمييز بين الربط الضربي والجمعي في قواعد النسختين المختلفتين من الربط: ففي حالة الربط الضربي (⊗)، يُقسّم سياق النتيجة ( Γ، Δ ) بين المقدمتين، بينما في حالة الربط الجمعي (&) ، يُنقل سياق النتيجة ( Γ ) كاملاً إلى كلتا المقدمتين.

الدوال الأسية

تُستخدم الدوال الأسية لتوفير تحكم دقيق في عمليات التضعيف والانكماش. وعلى وجه التحديد، نضيف قواعد هيكلية للتضعيف والانكماش للقضايا التي تبدأ بـ 'd: ^{[ 9 ]}

${\displaystyle \vdash }$Γ ${\displaystyle \vdash }$Γ،  ؟ أ

${\displaystyle \vdash }$Γ،  ؟ أ ،  ؟ أ ${\displaystyle \vdash }$Γ،  ؟ أ

واستخدم القواعد المنطقية التالية، حيث يمثل Γ قائمة من القضايا التي تبدأ كل منها بعلامة استفهام :

${\displaystyle \vdash }$؟Γ، أ ${\displaystyle \vdash }$؟Γ،  ! أ

${\displaystyle \vdash }$Γ، أ ${\displaystyle \vdash }$Γ،  ؟ أ

قد يلاحظ المرء أن قواعد الدوال الأسية تتبع نمطًا مختلفًا عن قواعد الروابط الأخرى، تشبه قواعد الاستدلال التي تحكم الأنماط في صياغات حساب التفاضل والتكامل المتتالي للمنطق النمطي العادي S4 ، وأنه لم يعد هناك تناظر واضح بين الثنائيات ! و ؟ . يتم تدارك هذا الوضع في العروض البديلة لـ CLL (مثل عرض LU ).

بالإضافة إلى ثنائيات دي مورغان الموضحة أعلاه، تتضمن بعض المكافئات المهمة في المنطق الخطي ما يلي:

التوزيعية

بحسب تعريف A ⊸ B على أنه A ^⊥ ⅋ B ، فإن قانوني التوزيع الأخيرين يعطيان أيضًا:

(هنا A ≣ B تعني ( A ⊸ B ) و ( B ⊸ A ) .)

التماثل الأسي

التوزيعات الخطية

الخريطة التي لا تُعدّ تماثلاً ولكنها تلعب دوراً حاسماً في المنطق الخطي هي:

تُعدّ التوزيعات الخطية أساسية في نظرية البرهان للمنطق الخطي. وقد دُرست نتائج هذه العلاقة لأول مرة في دراسة كوكيت وسيلي (1997) وأُطلق عليها اسم "التوزيع الضعيف". ^{[ 10 ]} وفي دراسات لاحقة، أُعيد تسميتها إلى "التوزيع الخطي" ليعكس ارتباطها الجوهري بالمنطق الخطي.

تداعيات أخرى

إن صيغ التوزيع التالية ليست تكافؤاً بشكل عام، بل هي مجرد استلزام:

يمكن استخلاص كل من الاستلزام الحدسي والكلاسيكي من الاستلزام الخطي بإدخال الدوال الأسية: يُشفّر الاستلزام الحدسي على النحو التالي : ! A ⊸ B ، بينما يُشفّر الاستلزام الكلاسيكي على النحو التالي : !? A ⊸  ? B أو ! A ⊸  ?! B (أو مجموعة متنوعة من الترجمات البديلة الممكنة). ^{[ 11 ]} الفكرة هي أن الدوال الأسية تسمح لنا باستخدام الصيغة عدة مرات حسب الحاجة، وهو أمر ممكن دائمًا في المنطق الكلاسيكي والحدسي.

بصورة رسمية، توجد ترجمة لصيغ المنطق الحدسي إلى صيغ المنطق الخطي بطريقة تضمن إمكانية إثبات الصيغة الأصلية في المنطق الحدسي إذا وفقط إذا كانت الصيغة المترجمة قابلة للإثبات في المنطق الخطي. وباستخدام ترجمة غودل-غينتزن السلبية ، يمكننا بالتالي دمج منطق الرتبة الأولى الكلاسيكي في منطق الرتبة الأولى الخطي.

طُوِّرت دلالات متعددة ومتميزة للمنطق الخطي، مما يعكس طبيعته المعقدة كنظام منطقي حساس للموارد. على عكس المنطق الكلاسيكي أو الحدسي، يميز المنطق الخطي بين الطرق المختلفة لدمج الصيغ، ويتعامل مع الافتراضات كموارد محدودة تُستهلك أثناء البرهان بدلاً من كونها قابلة للتكرار بلا حدود. ^{[ 5 ]}

تشمل المناهج الدلالية الرئيسية ما يلي:

دلالات الطور

نموذج مبكر يركز على إمكانية الإثبات.

الدلالات الفئوية

إطار جبري يُنمذج البراهين على أنها تشاكلات . الفئة المناسبة هي فئة فرعية من فضاء متجهي كامل ومنفصل وبورنولوجي مع تطبيقات خطية متصلة . ^{[ 12 ]}

دلالات اللعبة

نموذج تفاعلي يفسر الصيغ على أنها ألعاب والبراهين على أنها استراتيجيات. ^{[ 13 ]}

الدلالات الدلالية

نموذج يفسر البراهين على أنها كائنات رياضية. ^{[ 14 ]}

إن الدلالات الجبرية للمنطق الخطي هي دلالات الكميات .

في علم اللغة ، يُنمذج المنطق الخطي التحليل النحوي على أنه استنتاج . في هذه الحالة، تتوافق شجرة التحليل الصحيحة مع إثبات وجود جملة باستخدام قواعد الاستلزام التي تُشفّر القواعد النحوية. ^{[ 15 ]}

إن علاقة الاستلزام في لغة CLL الكاملة غير قابلة للتقرير . ^{[ 18 ]} عند النظر في أجزاء من لغة CLL، فإن مشكلة القرار لها تعقيد متفاوت:

• المنطق الخطي المضاعف (MLL): الروابط المضاعفة فقط. الاستلزام في MLL هو مسألة NP-كاملة ، حتى عند حصرها في عبارات هورن في الجزء الاستلزامي البحت، ^{[ 19 ]} أو في الصيغ الخالية من الذرات. ^{[ 20 ]}
• المنطق الخطي الضربي الجمعي (MALL): يقتصر على الضرب والجمع فقط (أي خالٍ من الدوال الأسية). الاستلزام في MALL هو مسألة كاملة في فضاء PSPACE . ^{[ 18 ]}
• المنطق الخطي المضاعف-الأسّي (MELL): يقتصر على المضاعفات والأسّيات. بالاختزال من مشكلة الوصول لشبكات بتري ، ^{[ 21 ]} يجب أن يكون الاستلزام في MELL على الأقل صعبًا من فئة EXPSPACE ، على الرغم من أن قابلية الحسم نفسها ظلت مشكلة مفتوحة لفترة طويلة. في عام 2015، نُشر برهان على قابلية الحسم في مجلة علوم الحاسوب النظرية ، ^{[ 22 ]} ولكن تبين لاحقًا أنه خاطئ. ^{[ 23 ]}
• لقد ثبت أن المنطق الخطي الأفيني (أي المنطق الخطي مع التضعيف، وهو امتداد وليس جزءًا) قابل للتقرير في عام 1995. ^{[ 24 ]}

تنشأ العديد من أشكال المنطق الخطي من خلال إجراء المزيد من التعديلات على القواعد الهيكلية:

• المنطق الأفيني ، الذي يمنع الانكماش ولكنه يسمح بالتضعيف العالمي (امتداد قابل للتقرير).
• المنطق الصارم أو منطق الصلة ، الذي يمنع الإضعاف ولكنه يسمح بالانكماش العالمي.
• المنطق غير التبادلي أو المنطق المرتب، الذي يلغي قاعدة التبادل، بالإضافة إلى منع التضعيف والانكماش. في المنطق المرتب، ينقسم الاستلزام الخطي إلى استلزام يساري واستلزام يميني.

تمّت دراسة العديد من المتغيرات الحدسية للمنطق الخطي. فعندما يُعتمد على تمثيل حسابي متتابع ذي نتيجة واحدة، كما هو الحال في المنطق الخطي الحدسي (ILL)،  تغيب الروابط ⅋ و⊥ و؟، ويُعامل الاستلزام الخطي كرابط بدائي. أما في المنطق الخطي الحدسي الكامل (FILL)،  فتوجد الروابط ⅋ و⊥ و؟، ويُعامل الاستلزام الخطي كرابط بدائي، وكما هو الحال في المنطق الحدسي، تكون جميع الروابط (باستثناء النفي الخطي) مستقلة. وهناك أيضًا امتدادات من الرتبة الأولى والرتب العليا للمنطق الخطي، والتي يُعدّ تطورها الرسمي معياريًا إلى حد ما (انظر منطق الرتبة الأولى ومنطق الرتب العليا ).

• مساحات تشو
• منطق قابلية الحوسبة
• دلالات اللعبة
• هندسة التفاعل
• المنطق الحدسي
• البرمجة المنطقية الخطية
• نظام النوع الخطي ، نظام النوع البنيوي الفرعي
• لوديكس
• شبكات الحماية
• أنواع الجلسات
• أنواع فريدة من نوعها

• بايز، جون ؛ ستاي، مايك (2008). بوب كويك (محرر). "الفيزياء، والطوبولوجيا، والمنطق، والحوسبة: حجر رشيد" (ملف PDF) . هياكل جديدة في الفيزياء .
• بيمبو، كاتالين (13 سبتمبر 2015). "قابلية حسم الجزء القصدي من المنطق الخطي الكلاسيكي" . علوم الحاسوب النظرية . 597 : 1-17 . doi : 10.1016/j.tcs.2015.06.019 . ISSN 0304-3975 . 
• كوكت، ج. روبن ؛ سيلي، روبرت (1997). "الفئات التوزيعية الضعيفة". مجلة الجبر البحت والتطبيقي . 114 (2): 133-173 . doi : 10.1016/0022-4049(95)00160-3 .
• دي كوزمو، روبرتو (1996). "2". مدخل إلى المنطق الخطي (ملاحظات الدورة).
• دي بايفا، V .؛ فان جينابيث، J .؛ ريتر، إي. (1999). “ندوة داغستوهل 99341 حول المنطق الخطي والتطبيقات” (PDF) . Drops-Idn/V2/Document/10.4230/Dagsemrep.248 . Schloss Dagstuhl – Leibniz-Zentrum für Informatik: 1– 21. doi : 10.4230/DagSemRep.248 .
• جيرارد، جان إيف (1987). "المنطق الخطي" (ملف PDF) . علوم الحاسوب النظرية . 50 (1): 1-102 . doi : 10.1016/0304-3975(87)90045-4 . hdl : 10338.dmlcz/120513 .
• غونتر، سي إيه؛ جيلوت، في. (1989). الشبكات كنظريات موترية (ملف PDF) (تقرير فني). جامعة بنسلفانيا. MS-CIS-89-68.
• كانوفيتش، ماكس آي. (22 يونيو 1992). "برمجة هورن في المنطق الخطي مسألة NP-كاملة". المؤتمر السنوي السابع لمعهد مهندسي الكهرباء والإلكترونيات حول المنطق في علوم الحاسوب ، 1992. LICS '92. وقائع المؤتمر. الصفحات 200-210 . doi : 10.1109/LICS.1992.185533 . ISBN  0-8186-2735-2.
• كوبيلوف، أ.ب. (1 يونيو 1995). "قابلية الحسم في المنطق الخطي الأفيني". الندوة السنوية العاشرة لمعهد مهندسي الكهرباء والإلكترونيات حول المنطق في علوم الحاسوب، 1995. LICS '95. وقائع الندوة السنوية العاشرة لمعهد مهندسي الكهرباء والإلكترونيات حول المنطق في علوم الحاسوب، 1995. LICS '95. وقائع الندوة. الصفحات 496-504 . CiteSeerX 10.1.1.23.9226 . doi : 10.1109/LICS.1995.523283 . ISBN   0-8186-7050-9.
• لينكولن، باتريك؛ ميتشل، جون؛ سيدروف، أندريه؛ شانكار، ناتاراجان (1992). "مسائل القرار في المنطق الخطي الافتراضي" . حوليات المنطق البحت والتطبيقي . 56 ( 1-3 ): 239-311 . doi : 10.1016/0168-0072(92)90075-B .
• لينكولن، باتريك؛ وينكلر، تيموثي (1994). "المنطق الخطي الضربي الثابت فقط هو مسألة NP-كاملة" . علوم الحاسوب النظرية . 135 : 155-169 . doi : 10.1016/0304-3975(94)00108-1 .
• ستراسبورغر، لوتز (10 مايو 2019). "حول مشكلة القرار لـ MELL" . علوم الحاسوب النظرية . 768 : 91-98 . doi : 10.1016/j.tcs.2019.02.022 . ISSN 0304-3975 . 

• المنطق الخطي في مختبر ن
• براونر، توربن (ديسمبر 1996). "مقدمة في المنطق الخطي" (ملف PDF) . سلسلة محاضرات بريكس. البحوث الأساسية في علوم الحاسوب (بريكس) . تاريخ الاسترجاع: 20 مايو 2025 .
• دي كوزمو، روبرتو؛ دانوس، فنسنت (1992). التمهيدي المنطق الخطي .
• دي كوزمو، روبرتو؛ ميلر، ديل (16 سبتمبر 2023). "المنطق الخطي" . في زالتا، إدوارد ن. (محرر). موسوعة ستانفورد للفلسفة (  طبعة خريف 2023). الرقم الدولي الموحد للدوريات 1095-5054 . رمز OCLC 429049174 .  
• جيرارد، جان إيف؛ لافون، إيف؛ تايلور، بول (1989). البراهين والأنواع . مطبعة جامعة كامبريدج. مؤرشف من الأصل في 4 يوليو 2016.
• هوار، سي. إيه. آر. (1985). التواصل بين العمليات المتسلسلة . برنتيس هول إنترناشونال. رقم ISBN 0-13-153271-5.
• لافون، إيف (1993). "مقدمة في المنطق الخطي". المدرسة الصيفية لبرنامج تيمبوس حول الأساليب الجبرية والفئوية في علوم الحاسوب (محاضرات). برنو، جمهورية التشيك.
• لينكولن، باتريك. "مقدمة في المنطق الخطي" (ملحق) .
• ميلر، ديل (2004). "نظرة عامة على برمجة المنطق الخطي". في: إيرهارد؛ جيرارد؛ رويت؛ سكوت (محررون). المنطق الخطي في علوم الحاسوب (ملف PDF) . سلسلة محاضرات الجمعية الرياضية بلندن. المجلد  316. مطبعة جامعة كامبريدج.
• ترولسترا، أ.س. (1992). محاضرات في المنطق الخطي . سلسلة محاضرات مركز دراسات المنطق الخطي. المجلد  29. ستانفورد: منشورات مركز دراسات المنطق الخطي. رقم ISBN 978-0937073773.
• ترولسترا، أ.س .؛ شفيتشتنبرغ، هـ. (2000) [1996]. نظرية البرهان الأساسية . سلسلة كامبريدج في علوم الحاسوب النظرية. المجلد  43 (  الطبعة الثانية). كامبريدج: مطبعة جامعة كامبريدج. الصفحات  12، 417. doi : 10.1017/CBO9781139168717 . ISBN 9780521779111. OCLC 951181823 . 
• وادلر، فيليب. "لمحة عن المنطق الخطي" .

• الوسائط المتعلقة بالمنطق الخطي على ويكيميديا ​​كومنز
• برنامج إثبات المنطق الخطي (llprover)، مؤرشف بتاريخ 4 أبريل 2016 على موقع Wayback Machine ، متاح للاستخدام عبر الإنترنت، من: ناويوكي تامورا / قسم علوم الحاسوب / جامعة كوبي / اليابان
• أداة إثبات المنطق الخطي التفاعلية " انقر واستلم" ، متوفرة عبر الإنترنت
• لوبيز، أديل (7 يونيو 2020). "المنطق الخطي المرئي" . — حساب مرئي للعبارات والاستنتاج في المنطق الخطي