Съдържание 
 

ТЕРМОВЕ ПРИ ДАДЕНА СИГНАТУРА

      В текста „Сигнатури и структури“ предположихме, че е избрано едно безкрайно множество от думи над основната азбука, които се уславяме да наричаме допустими сигнатурни символи, и при това съществуват безбройно много думи над същата азбука със свойството никой техен непразен край да не е начало на допустим сигнатурен символ. Пак там видяхме, че непразните думи с това свойство не могат да бъдат допустими сигнатурни символи. Оттук нататък ще предполагаме още, че е избрано едно безкрайно множество Ξ от непразни думи със споменатото свойство, а думите от това множество ще наричаме променливи. В условията на пример 1 от текста „Сигнатури и структури“ можем в качеството на променливи да вземем думите с главна латинска буква в началото и някакъв (евентуално нулев) брой цифри след нея, а в условията на пример 2 от въпросния текст  –  думите с някоя от последните шест малки латински букви в началото и някакъв (евентуално нулев) брой цифри след нея (в конкретните примери по-нататък ще се придържаме именно към този вариант). Добре е да отбележимм, че езикът Пролог и програмата Prover 9, с които са свързани двата варианта и при които не се изисква да е непременно налице припомненото по-горе допълнително свойство, допускат доста повече конкретни думи като променливи, отколкото допуснахме ние.

      Нека е дадена една сигнатура Σ. Ще дефинираме понятието терм при сигнатура Σ, като всеки такъв терм ще бъде дума над основната азбука, разширена чрез добавяне на двете скоби и запетаята. Дефиницията е индуктивна и се състои от следните три точки:
        0. Всяка променлива е терм при сигнатура Σ.
        1. Всяка константа на Σ е терм при сигнатура Σ.
        2. Винаги, когато m е положително цяло число, ω e m-местен функционален символ на Σ и τ1, …, τm са термове при сигнатура Σ, думата  ω(τ1,…,τm)  също е терм при сигнатура Σ.

      Забележка 1. Както беше при дефиницията на понятието затворен терм, и тук скобите и запетаите фигурират в означението  ω(τ1,…,τm)  като формални символи и не означават нищо друго освен самите себе си.

      Пример. Думата   difference(difference(one,one),x))  е терм при сигнатурата Σ′ от пример 3 в текста „Сигнатури и структури“.

      Чрез индукция, съобразена с дефиницията на понятието затворен терм, веднага се вижда, че всеки затворен терм при дадена сигнатура е терм при тази сигнатура. Обратното очевидно не е вярно (например променливите не са затворени термове).

      Забележка 2. В съгласие със забележка 3 от текста „Сигнатури и структури“ вместо „терм в сигнатура Σ“, „константа на Σ“ и „функционален символ на Σ“ често ще пишем само „терм“, „константа“ и „функционален символ“. В частност така ще постъпваме по-нататък в настоящия текст.

      Дадената индуктивна дефиниция позволява да доказваме общи свойства на термовете с помощта на индукция, съобразена с нея. А именно, за да докажем, че всеки терм има дадено свойство, достатъчно е да покажем от една страна, че то е налице за променливите и за константите, и от друга, че то се запазва при прилагането на последната точка от дефиницията (т.е. винаги, когато m е положително цяло число, ω e m-местен функционален символ и τ1, …, τm са термове, притежаващи даденото свойство, термът  ω(τ1,…,τm)  също го притежава). По такъв начин може да се докаже например, че всеки терм е силно приемлива дума в смисъла на текста „Осигуряване на еднозначен прочит с помощта на скоби и разделители“ при азбука Α, съвпадаща с основната, и азбука Β, получена от нея чрез добавяне на скобите и запетаята. Оттук по начин, аналогичен на онзи за затворените термове, можем да докажем, че при дадената дефиниция за терм е налице еднозначен прочит на термовете, т.е. всеки терм може да бъде получен само по една от трите точки на дефиницията, и то само по един начин.

Последно изменение: 7.11.2008 г.