رمز الدالة

في الأنظمة الرسمية، وخاصة المنطق الرياضي ، يُعد رمز الدالة رمزًا غير منطقي يُمثل دالة أو تطبيقًا على مجال الخطاب ، مع أنه، من الناحية الرسمية، لا يُشترط أن يُمثل أي شيء على الإطلاق. تُعد رموز الدوال عنصرًا أساسيًا في اللغات الرسمية لتكوين المصطلحات . تحديدًا، إذا كان الرمز${\displaystyle F}$إذا كان رمز دالة، فإنه عند إعطاء أي رمز ثابت${\displaystyle X}$تمثيل كائن في اللغة،${\displaystyle F(X)}$كما يمثل كائنًا في اللغة. وبالمثل، إذا${\displaystyle T}$هو مصطلح ما في اللغة،${\displaystyle F(T)}$هو أيضاً مصطلح. ولذلك، يجب تعريف تفسير رمز الوظيفة على نطاق الخطاب بأكمله. رموز الوظائف مفهوم أولي ، وبالتالي لا تُعرَّف بدلالة مفاهيم أخرى أكثر أساسية.

في المنطق المكتوب ، يُعتبر F رمزًا وظيفيًا من نوع المجال T ونوع المجال المقابل U إذا كان، لأي رمز X يمثل كائنًا من النوع T ، فإن F ( X ) هو رمز يمثل كائنًا من النوع U. وبالمثل، يمكن تعريف رموز الدوال التي تحتوي على أكثر من متغير واحد، على غرار الدوال التي تحتوي على أكثر من متغير واحد؛ أما رمز الدالة الذي لا يحتوي على أي متغيرات فهو ببساطة رمز ثابت.

لنفترض الآن نموذجًا للغة الرسمية، حيث يتم تمثيل النوعين T و U بالمجموعتين [ T ] و [ U ]، ويتم تمثيل كل رمز X من النوع T بالعنصر [ X ] في [ T ]. عندئذٍ ، يمكن تمثيل F بالمجموعة

${\displaystyle [F]:={\big \{}([X],[F(X)]):[X]\in [\mathbf {T} ]{\big \}},}$

وهي ببساطة دالة ذات مجال [ T ] ومجال مقابل [ U ]. ومن متطلبات النموذج المتسق أن يكون [ F ( X )] = [ F ( Y )] كلما كان [ X ] = [ Y ].

في معالجة منطق المسندات التي تسمح بإدخال رموز مسندات جديدة، سيُرغب أيضًا في إمكانية إدخال رموز دوال جديدة. بمعرفة رمزي الدالتين F و G ، يمكن تعريف رمز دالة جديد F ∘ G ، وهو تركيب F و G ، بحيث يحقق الشرط ( F ∘ G )( X ) = F ( G ( X ))، لكل X. بالطبع، لا يكون للطرف الأيمن من هذه المعادلة معنى في المنطق المكتوب إلا إذا تطابق نوع مجال F مع نوع المجال المقابل لـ G ، وهذا شرط أساسي لتعريف التركيب.

يُستَخدَم أيضًا بعض رموز الدوال تلقائيًا. في المنطق غير المُصنَّف، توجد دالة هوية id تُحقِّق الشرط id( X ) = X لجميع قيم X. في المنطق المُصنَّف، لأي نوع T ، توجد دالة هوية idT _بنوع المجال والمجال المقابل T ؛ تُحقِّق الشرط idT ₍ X ) = X لجميع قيم X من النوع T. وبالمثل، إذا كان T نوعًا فرعيًا من U ، فستوجد دالة تضمين بنوع المجال T ونوع المجال المقابل U تُحقِّق المعادلة نفسها؛ وتوجد رموز دوال إضافية مرتبطة بطرق أخرى لإنشاء أنواع جديدة من أنواع قديمة.

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

لكل X من النوع T ، ولبعض Y الفريدة من النوع U ، P ( X , Y )،

عندئذٍ يمكنك تعريف رمز دالة F من نوع المجال T ونوع المجال المقابل U الذي يحقق ما يلي:

لكل X من النوع T ، ولكل Y من النوع U ، P ( X , Y ) إذا وفقط إذا كان Y = F ( X ).

لا تسمح العديد من معالجات منطق المسندات بالمسندات الوظيفية، بل بالمسندات العلائقية فقط . وهذا مفيد، على سبيل المثال، في سياق إثبات النظريات الميتافيزيقية (مثل نظريات عدم الاكتمال لغودل )، حيث لا يُراد السماح بإدخال رموز وظيفية جديدة (ولا أي رموز جديدة أخرى). ولكن توجد طريقة لاستبدال الرموز الوظيفية بالرموز العلائقية أينما وُجدت؛ علاوة على ذلك، فإن هذه الطريقة خوارزمية، وبالتالي فهي مناسبة لتطبيق معظم النظريات الميتافيزيقية على النتيجة.

على وجه التحديد، إذا كان للدالة F نوع المجال T ونوع المجال المقابل U ، فيمكن استبدالها بمسند P من النوع ( T , U ). وبشكل بديهي، فإن P ( X , Y ) تعني F ( X ) = Y. بالتالي، كلما ظهرت F ( X ) في عبارة، يمكنك استبدالها برمز جديد Y من النوع U وإضافة عبارة أخرى P ( X , Y ). وللوصول إلى نفس الاستنتاجات، تحتاج إلى قضية إضافية.

لكل X من النوع T ، لبعض Y الفريدة من النوع U ، P ( X ، Y ).

(بالطبع، هذا هو نفس الافتراض الذي كان يجب إثباته كنظرية قبل تقديم رمز دالة جديد في القسم السابق.)

نظرًا لأن حذف المسندات الوظيفية يُعدّ مناسبًا لبعض الأغراض وممكنًا، فإن العديد من معالجات المنطق الصوري لا تتناول رموز الدوال صراحةً، بل تستخدم رموز العلاقات فقط. ويمكن النظر إلى هذا الأمر من زاوية أخرى، وهي أن المسند الوظيفي نوع خاص من المسندات، وتحديدًا المسند الذي يحقق القضية المذكورة أعلاه. قد يبدو هذا إشكالًا إذا أردنا تحديد مخطط قضية ينطبق فقط على المسندات الوظيفية F ؛ فكيف لنا أن نعرف مسبقًا ما إذا كان يحقق هذا الشرط؟ للحصول على صياغة مكافئة للمخطط، نستبدل أولًا أي شيء من الشكل F ( X ) بمتغير جديد Y. ثم نُعمّم على كل Y مباشرةً بعد إدخال X المقابل (أي بعد تعميم X ، أو في بداية العبارة إذا كان X حرًا)، ونحمي التعميم بـ P ( X , Y ). أخيرًا، نجعل العبارة بأكملها نتيجة مادية لشرط التفرد للمسند الوظيفي المذكور أعلاه.

لنأخذ كمثال مخطط بديهيات الاستبدال في نظرية مجموعات زيرميلو-فرانكل . (يستخدم هذا المثال رموزًا رياضية ). ينص هذا المخطط (بصيغة واحدة) على أنه لأي دالة منطقية F في متغير واحد:

${\displaystyle \forall A,\exists B,\forall C,C\in A\rightarrow F(C)\in B.}$

أولاً، يجب علينا استبدال F ( C ) بمتغير آخر D :

${\displaystyle \forall A,\exists B,\forall C,C\in A\rightarrow D\in B.}$

بالطبع، هذه العبارة غير صحيحة؛ يجب تحديد كمية D بعد C مباشرة :

${\displaystyle \forall A,\exists B,\forall C,\forall D,C\in A\rightarrow D\in B.}$

لا يزال يتعين علينا إدخال P لحماية هذا التحديد الكمي:

${\displaystyle \forall A,\exists B,\forall C,\forall D,P(C,D)\rightarrow (C\in A\rightarrow D\in B).}$

هذا صحيح تقريبًا، لكنه ينطبق على عدد كبير جدًا من المسندات؛ ما نريده في الواقع هو:

${\displaystyle (\forall X,\exists !Y,P(X,Y))\rightarrow (\forall A,\exists B,\forall C,\forall D,P(C,D)\rightarrow (C\in A\rightarrow D\in B)).}$

هذه النسخة من مخطط البديهيات للاستبدال مناسبة الآن للاستخدام في لغة رسمية لا تسمح بإدخال رموز دوال جديدة. وبدلاً من ذلك، يمكن تفسير العبارة الأصلية كعبارة في مثل هذه اللغة الرسمية؛ فهي مجرد اختصار للعبارة الناتجة في النهاية.

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

(declare-fun f (Int) Int) (assert (= (f 10) 1)) 

(declare-fun f (Int) Int) (assert (= (f 10) 1)) (assert (= (f 10) 42)) 

• نوع البيانات الجبرية
• الجبر الابتدائي
• الرابط المنطقي
• ثابت منطقي
• جبر المصطلحات
• نظرية المساواة المطلقة