Avaldiste võrduse tuvastamisest

Avaldiste all mõistame siin avaldisi, mis on moodustatud muutujatest, mingi hulga konkreetsete elementide tähistest ja selle hulgal defineeritud konkreetsete funktsioonide tähistest.

Parajasti lubatud konstant- ja funktsionaalsümbolite hulka nimetame ka signatuuriks.

Kõige rohkem pakub huvi juht, kus muutujate määramispiirkonnaks on reaalarvude hulk või ka kompleksarvude hulk ja funktsionaalsümbolid tähistavad mingeid elementaarfunktsioone.

Olukorra teeb mõnevõrra keerulisemaks see, et vaatluse all võivad olla ka vaadeldaval hulgal mitte kõikjal defineeritud funktsioonid: jagamine, tangens, logaritm, juured jms.

Matemaatilistes tekstides me mõistame avaldiste võrdust

s(x₁,...,x_n) = t(x₁,...,x_n)

kui võrdust, mille ees on üldisuse kvantorid. Kuna ühe või teise avaldise väärtus võib olla mingitel argumendi väärtustel ka mitte defineeritud, siis: kui üks on defineeritud, siis ka teine ja kehtib võrdus.  

Avaldiste võrduse kontroll on matemaatikas tihti vajalik:

- tõestuste lugemine,

- õpilaste tööde kontrollimine.

Oleks hea, kui meie käsutuses oleks algoritm avaldiste võrduse kontrolliks. Osutub, et mõnel juhul on see võimalik, mõnel juhul võimatu.

1. Lausearvutuse valemite samaväärsust saab kontrollida  tõeväärtustabeli abil.
2. Predikaatloogika valemite samaväärsus ei ole algoritmiliselt lahenduv (Church, 1936).
3. Hulkliikmete võrdust saab kontrollida kanoonilisele kujule viimise abil.
4. Avaldiste võrdus signatuuris, mis sisaldab täisarve, liitmist, korrutamist, sin ja absoluutväärtust, on mittelahenduv (Richardson, 1968).

<>Viimane tulemus jätab aga probleemi isegi keskkoolimatemaatika paljude valdkondade jaoks vastuseta. Ühelt poolt on siin tegemist üsna väikese signatuuriga, teiselt poolt sisaldab ta aga absoluutväärtust, mida kasutame küllalt harva. On ilmne, et iga tulemus mingi muu funktsioonide komplekti kohta oleks huvipakkuv.

Olen küsinud paljude arvutialgebra autoriteetide (Davenport, Buchberger, Calmet, Matijasevitš, ...) käest, kas nad teavad tulemusi muude signatuuride kohta. Seni on vastus olnud eitav. Richardsoni tõestuses on absoluutväärtuse kasutamine oluline.

Vähemalt pidevate funktsioonide korral on mittevõrdus rekursiivselt loetletav. Kui avaldised pole võrdsed, siis võime arvutada nende väärtusi kõikjal tiheda loenduva hulga elementidel, kuni saame erinevuse. Aga:

- kõik vaadeldavad funktsioonid pole pidevad,

- mõnikord on erinevused ainult lõplikus arvus punktides: 2x/x ei ole  2 ainult punktis 0,

- funktsiooni väärtuse arvutamine mingis punktis võib olla mittetriviaalne (fakt, et funktsioon pole antud punktis määratud, ei tarvitse selguda lõpliku arvu sammudega).

Teiselt poolt võime üritada tõestada teadaolevate samasuste abil avalduste võrdumist. Osutub aga, et mõned kehtivad võrdused pole tõestatavad samasusteisenduste abil (aga on näiteks induktsiooniga).

Arvutialgebra süsteemidest on avaldiste võrdusega tõsisemalt tegelnud Maple’i autorid. Teistes süsteemides spetsiaalseid võrduse kontrolli primitiive eriti pole, tuleb rakendada kahe avaldise vahe lihtsustamist ja vaadata, kas tulemuseks on 0. Arvuliste avaldiste korral ongi võrduse probleem ekvivalentne nulliga võrdumise probleemiga.

Peale avaldiste samaväärsuse tuleb matemaatikas tegelda ka võrrandite ja võrrandisüsteemide samaväärsusega. See valdkond on veel keerulisem.