تابع تفسیرنشده

یک تابع تفسیرنشده^[۱] (به انگلیسی: uninterpreted function)، یا نماد تابعی^[۲] (به انگلیسی: function symbol) در منطق ریاضی، یعنی تابعی که هیچ ویژگی دیگری بجز «نام» و «تعداد عملوند» (آریتی) ندارد. از «نمادهای تابعی» همراه با ثابت‌ها و متغیرها استفاده می‌شود تا یک «تِرم» را بسازیم.

به نظریه توابع تفسیرنشده گاهی نظریه آزاد هم گفته می‌شود، زیرا به صورت آزاد تولید می‌شود، یک شیء آزاد یا نظریه خالی، یعنی نظریه‌ای که مجموعه جمله‌هایش خالی باشد (در مقایسه با جبر اولیه). نظریه‌هایی که مجموعه معادله غیرتهی دارند، «نظریه‌های معادله‌ای» نامیده می‌شوند. مسئله رضایت برای نظریه‌های آزاد توسط یکسان‌سازی نحوی حل می‌گردند؛ «الگوریتم‌های یکسان‌سازی نحوی» توسط مفسرهای زبان رایانه‌ای متنوع، مثلاً پرولوگ، استفاده می‌شوند. یکسان‌سازی نحوی همچنین در مسئله رضایت برای نظریه‌های معادله‌ای معین دیگری، مثل یکسان‌سازی E و محدودسازی هم استفاده می‌شوند.

مثال

به عنوان یک مثال از توابع تفسیرنشده برای SMT-LIB، ما به یک حل‌کننده SMT این ورودی را می‌دهیم:

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

حل‌کننده SMT جواب «این ورودی راضی‌کننده است» را برخواهد گرداند. این موضوع به این دلیل رخ می‌دهد که f یک تابع تفسیرنشده است (یعنی همه آنچه دربارهٔ f می‌دانیم، امضای آن است) بنابراین امکان آن وجود دارد که f(10) = 1 اما با اعمال ورودی زیر:

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

حل کننده SMT برمی‌گرداند که «ورودی راضی‌کننده نیست». این موضوع به این دلیل رخ داده‌است که اگرچه f تفسیری ندارد، اما این که یک تابع برای ورودی‌های مشابه مقادیر متفاوتی را برگرداند، غیرممکن است.

بحث

مسئله تصمیم‌گیری برای «نظریه‌های آزاد» به‌طور ویژه مهم است، زیرا بسیاری از نظریه‌ها را می‌توان با آن کاهش داد.

نظریه‌های آزاد را می‌توان با جستجو برای زیرعبارات مشترک با هدف ساخت بستار همنهشت حل کرد. این حل‌کننده‌ها شامل حل کننده رضایت بر پیمانه نظریه هم هستند.

پانویس

↑ Bryant, Randal E.; Lahiri, Shuvendu K.; Seshia, Sanjit A. (2002). "Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions" (PDF). Computer Aided Verification. Lecture Notes in Computer Science. Vol. 2404. pp. 78–92. doi:10.1007/3-540-45657-0_7. ISBN 978-3-540-43997-4.
↑ Baader, Franz; Nipkow, Tobias (1999). Term Rewriting and All That. Cambridge University Press. p. 34. ISBN 978-0-521-77920-3.

منابع

مشارکت‌کنندگان ویکی‌پدیا. «Uninterpreted function». در دانشنامهٔ ویکی‌پدیای انگلیسی، بازبینی‌شده در ۲۷ آوریل ۲۰۲۱.

[1] Bryant, Randal E.; Lahiri, Shuvendu K.; Seshia, Sanjit A. (2002). "Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions" (PDF). Computer Aided Verification. Lecture Notes in Computer Science. Vol. 2404. pp. 78–92. doi:10.1007/3-540-45657-0_7. ISBN 978-3-540-43997-4.

[2] Baader, Franz; Nipkow, Tobias (1999). Term Rewriting and All That. Cambridge University Press. p. 34. ISBN 978-0-521-77920-3.

[۱]

[۲]