Otolkad funktion

I matematisk logik är en otolkad funktion eller funktionssymbol en som inte har någon annan egenskap än dess namn och n-ära form. Funktionssymboler används, tillsammans med konstanter och variabler, för att bilda termer .

Teorin om otolkade funktioner kallas också ibland för den fria teorin , eftersom den genereras fritt, och därmed ett fritt objekt , eller den tomma teorin , som är teorin som har en tom uppsättning meningar (i analogi med en initial algebra ). Teorier med en icke-tom uppsättning ekvationer kallas ekvationsteorier . Tillfredsställbarhetsproblemet fria teorier löses genom syntaktisk enande ; algoritmer för de senare används av tolkar för olika datorspråk, som Prolog . Syntaktisk unifiering används också i algoritmer för tillfredsställbarhetsproblemet för vissa andra ekvationsteorier, se Unification (datavetenskap) .

Exempel

Som ett exempel på otolkade funktioner för SMT-LIB, om denna ingång ges till en SMT-lösare :

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

SMT-lösaren skulle returnera "Denna ingång är tillfredsställande". Det händer eftersom f är en otolkad funktion (dvs allt som är känt om f är dess signatur ), så det är möjligt att f(10) = 1 . Men genom att använda inmatningen nedan:

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

SMT-lösaren skulle returnera "Denna ingång är otillfredsställande". Det händer eftersom f , som är en funktion, aldrig kan returnera olika värden för samma ingång.

Diskussion

Beslutsproblemet för fria teorier är särskilt viktigt, eftersom många teorier kan reduceras av det .

Fria teorier kan lösas genom att söka efter vanliga deluttryck för att bilda kongruensslutningen . Lösare inkluderar satisfiability modulo teorier lösare.

Se även

• Algebraisk datatyp
• Initial algebra
• Term algebra
• Teori om ren jämlikhet