SICP · Yr ail argraffiad · Scheme

4.4 Rhaglennu Rhesymegol

Harold Abelson a Gerald Jay Sussman gyda Julie Sussman · Cyfieithiad Cymraeg

Ym Mhennod 1 pwysleisiwyd bod cyfrifiadureg yn ymdrin â gwybodaeth orchmynnol (sut i wneud), tra bo mathemateg yn ymdrin â gwybodaeth ddatganiadol (beth yw). Yn wir, mae ieithoedd rhaglennu yn mynnu bod y rhaglennydd yn mynegi gwybodaeth mewn ffurf sy'n dangos y dulliau cam wrth gam ar gyfer datrys problemau penodol. Ar y llaw arall, mae ieithoedd lefel uchel yn darparu, fel rhan o weithrediad yr iaith, swm sylweddol o wybodaeth am ddulliau sy'n rhyddhau'r defnyddiwr rhag poeni am fanylion niferus sut y bydd cyfrifiad penodedig yn mynd rhagddo.

Mae'r rhan fwyaf o ieithoedd rhaglennu, gan gynnwys Lisp, wedi'u trefnu o amgylch cyfrifo gwerthoedd ffwythiannau mathemategol. Mae ieithoedd sy'n canolbwyntio ar fynegiadau (megis Lisp, Fortran, ac Algol) yn manteisio ar y “chwarae ar eiriau” y gellir dehongli mynegiad sy'n disgrifio gwerth ffwythiant hefyd fel modd o gyfrifo'r gwerth hwnnw. Oherwydd hyn, mae'r rhan fwyaf o ieithoedd rhaglennu yn tueddu'n gryf at gyfrifiadau uncyfeiriol (cyfrifiadau â mewnbynnau ac allbynnau wedi'u diffinio'n glir). Fodd bynnag, ceir ieithoedd rhaglennu cwbl wahanol sy'n llacio'r duedd hon. Gwelsom un enghraifft o'r fath yn 3.3.5, lle'r oedd gwrthrychau'r cyfrifiannu yn gyfyngiadau rhifyddol. Mewn system gyfyngiadau, nid yw cyfeiriad a threfn y cyfrifiannu wedi'u pennu mor glir; wrth gyflawni cyfrifiad rhaid i'r system felly ddarparu gwybodaeth “sut i wneud” fanylach nag yn achos cyfrifiad rhifyddol arferol. Nid yw hyn yn golygu, fodd bynnag, fod y defnyddiwr yn cael ei ryddhau'n llwyr o'r cyfrifoldeb o ddarparu gwybodaeth orchmynnol. Ceir llawer o rwydweithiau cyfyngiadau sy'n gweithredu'r un set o gyfyngiadau, a rhaid i'r defnyddiwr ddewis rhwydwaith addas o blith y rhwydweithiau sy'n fathemategol gyfwerth er mwyn pennu cyfrifiad penodol.

Mae gwerthusydd rhaglenni an-benderfyniaethol 4.3 hefyd yn symud oddi wrth y safbwynt mai adeiladu algorithmau ar gyfer cyfrifo ffwythiannau uncyfeiriol yw rhaglennu. Mewn iaith an-benderfyniaethol, gall mynegiadau gael mwy nag un gwerth, ac, o ganlyniad, mae'r cyfrifiad yn ymdrin â pherthnasoedd yn hytrach na ffwythiannau unwerth. Mae rhaglennu rhesymegol yn ymestyn y syniad hwn drwy gyfuno golwg berthynol ar raglennu â math pwerus o baru patrymau symbolaidd a elwir yn uno patrymau.²⁶²

Gall y dull hwn, pan fydd yn gweithio, fod yn ffordd bwerus iawn o ysgrifennu rhaglenni. Daw rhan o'r grym o'r ffaith y gellir defnyddio un ffaith “beth yw” i ddatrys nifer o broblemau gwahanol a fyddai â chydrannau “sut i wneud” gwahanol. Er enghraifft, ystyriwch y gweithrediad append, sy'n cymryd dwy restr fel argiau ac yn cyfuno eu helfennau i ffurfio un rhestr. Mewn iaith weithdrefnol megis Lisp, gallem ddiffinio append yn nhermau'r adeiladydd rhestrau sylfaenol cons, fel y gwnaethom yn 2.2.1:

(define (append x y)
  (if (null? x) 
      y 
      (cons (car x) (append (cdr x) y))))

Gellir ystyried y weithdrefn hon yn gyfieithiad i Lisp o'r ddwy reol ganlynol, y gyntaf ohonynt yn ymdrin â'r achos lle mae'r rhestr gyntaf yn wag, a'r ail yn ymdrin ag achos rhestr ddiwag, sef cons o ddwy ran:

Ar gyfer unrhyw restr y, mae'r rhestr wag ac y yn cyfuno drwy append i ffurfio y.
Ar gyfer unrhyw u, v, y, ac z, mae (cons u v) ac y yn cyfuno drwy append i ffurfio (cons u z) os yw v ac y yn cyfuno drwy append i ffurfio z.²⁶³

Gan ddefnyddio'r weithdrefn append, gallwn ateb cwestiynau megis

Darganfyddwch append rhestrau (a b) ac (c d).

Ond mae'r un ddwy reol hefyd yn ddigonol i ateb y mathau canlynol o gwestiynau, na all y weithdrefn eu hateb:

Darganfyddwch restr y sy'n cyfuno drwy append ag (a b) i gynhyrchu (a b c d).

Darganfyddwch bob x ac y sy'n cyfuno drwy append i ffurfio (a b c d).

Mewn iaith raglennu resymegol, mae'r rhaglennydd yn ysgrifennu “gweithdrefn” append drwy ddatgan y ddwy reol am append a roddir uchod. Darperir gwybodaeth “sut i wneud” yn awtomatig gan y dehonglydd i ganiatáu defnyddio'r un pâr hwn o reolau i ateb pob un o'r tri math o gwestiwn am append.²⁶⁴

Mae gan ieithoedd rhaglennu rhesymegol cyfoes (gan gynnwys yr un a weithredwn yma) ddiffygion sylweddol, gan y gall eu dulliau “sut i wneud” cyffredinol eu harwain i ddolenni anfeidraidd diangen neu ymddygiad annymunol arall. Mae rhaglennu rhesymegol yn faes ymchwil gweithgar mewn cyfrifiadureg.²⁶⁵

Yn gynharach yn y bennod hon archwiliwyd technoleg gweithredu dehonglwyr a disgrifiwyd yr elfennau sy'n hanfodol i ddehonglydd ar gyfer iaith debyg i Lisp (yn wir, i ddehonglydd ar gyfer unrhyw iaith gonfensiynol). Nawr byddwn yn cymhwyso'r syniadau hyn i drafod dehonglydd ar gyfer iaith raglennu resymegol. Galwn yr iaith hon yn iaith ymholi, oherwydd ei bod yn ddefnyddiol iawn ar gyfer adalw gwybodaeth o gronfeydd data drwy lunio ymholiadau, neu gwestiynau, wedi'u mynegi yn yr iaith. Er bod yr iaith ymholi'n wahanol iawn i Lisp, byddwn yn gweld ei bod yn gyfleus disgrifio'r iaith yn nhermau'r un fframwaith cyffredinol yr ydym wedi'i ddefnyddio drwy'r amser: fel casgliad o elfennau cyntefig, ynghyd â dulliau cyfuno sy'n ein galluogi i gyfuno elfennau syml i greu elfennau mwy cymhleth a dulliau haniaethu sy'n ein galluogi i ystyried elfennau cymhleth yn unedau cysyniadol unigol. Mae dehonglydd ar gyfer iaith raglennu resymegol gryn dipyn yn fwy cymhleth na dehonglydd ar gyfer iaith fel Lisp. Serch hynny, fe welwn fod ein dehonglydd iaith ymholi'n cynnwys llawer o'r un elfennau a geir yn nehonglydd 4.1. Yn benodol, bydd rhan “eval” sy'n dosbarthu mynegiadau yn ôl math a rhan “apply” sy'n gweithredu mecanwaith haniaethu'r iaith (gweithdrefnau yn achos Lisp, a rheolau yn achos rhaglennu rhesymegol). Hefyd, chwaraeir rôl ganolog yn y gweithrediad gan strwythur data ffrâm, sy'n pennu'r cyfatebiaeth rhwng symbolau a'u gwerthoedd cysylltiedig. Un agwedd ddiddorol ychwanegol ar ein gweithrediad iaith ymholi yw ein bod yn gwneud defnydd sylweddol o ffrydiau, a gyflwynwyd ym Mhennod 3.

4.4.1Adalw Gwybodaeth drwy Ddiddwytho

Mae rhaglennu rhesymegol yn rhagori wrth ddarparu rhyngwynebau i gronfeydd data ar gyfer adalw gwybodaeth. Mae'r iaith ymholi y byddwn yn ei gweithredu yn y bennod hon wedi'i dylunio i'w defnyddio fel hyn.

Er mwyn dangos beth mae'r system ymholi'n ei wneud, byddwn yn dangos sut y gellir ei defnyddio i reoli cronfa ddata cofnodion personél Microshaft, cwmni technoleg uchel ffyniannus yn ardal Boston. Mae'r iaith yn darparu mynediad at wybodaeth personél wedi'i gyfarwyddo gan batrymau, a gall hefyd fanteisio ar reolau cyffredinol er mwyn gwneud diddwythiadau rhesymegol.

Cronfa ddata enghreifftiol

Mae cronfa ddata personél Microshaft yn cynnwys haeriadau am bersonél y cwmni. Dyma'r wybodaeth am Ben Bitdiddle, dewin cyfrifiaduron y cwmni:

(address (Bitdiddle Ben) 
         (Slumerville (Ridge Road) 10))
(job (Bitdiddle Ben) (computer wizard))
(salary (Bitdiddle Ben) 60000)

Mae pob haeriad yn rhestr (tripled yn yr achos hwn) y gall ei helfennau eu hunain fod yn restrau.

Fel dewin y cwmni, Ben sydd â gofal dros yr adran gyfrifiaduron, ac mae'n goruchwylio dau raglennydd ac un technegydd. Dyma'r wybodaeth amdanynt:

(address (Hacker Alyssa P) 
         (Cambridge (Mass Ave) 78))
(job (Hacker Alyssa P) (computer programmer))
(salary (Hacker Alyssa P) 40000)
(supervisor (Hacker Alyssa P) (Bitdiddle Ben))

(address (Fect Cy D) 
         (Cambridge (Ames Street) 3))
(job (Fect Cy D) (computer programmer))
(salary (Fect Cy D) 35000)
(supervisor (Fect Cy D) (Bitdiddle Ben))

(address (Tweakit Lem E) 
         (Boston (Bay State Road) 22))
(job (Tweakit Lem E) (computer technician))
(salary (Tweakit Lem E) 25000)
(supervisor (Tweakit Lem E) (Bitdiddle Ben))

Mae yna hefyd raglennydd dan hyfforddiant, a oruchwylir gan Alyssa:

(address (Reasoner Louis) 
         (Slumerville (Pine Tree Road) 80))
(job (Reasoner Louis) 
     (computer programmer trainee))
(salary (Reasoner Louis) 30000)
(supervisor (Reasoner Louis) 
            (Hacker Alyssa P))

Mae'r holl bobl hyn yn yr adran gyfrifiaduron, fel y dangosir gan y gair computer fel yr eitem gyntaf yn eu disgrifiadau swydd.

Mae Ben yn gyflogai ar lefel uchel. Ei oruchwyliwr yw pennaeth mawr y cwmni ei hun:

(supervisor (Bitdiddle Ben) (Warbucks Oliver))
(address (Warbucks Oliver) 
         (Swellesley (Top Heap Road)))
(job (Warbucks Oliver) 
     (administration big wheel))
(salary (Warbucks Oliver) 150000)

Yn ogystal â'r adran gyfrifiaduron a oruchwylir gan Ben, mae gan y cwmni adran gyfrifyddu, sy'n cynnwys prif gyfrifydd a'i gynorthwyydd:

(address (Scrooge Eben) 
         (Weston (Shady Lane) 10))
(job (Scrooge Eben) 
     (accounting chief accountant))
(salary (Scrooge Eben) 75000)
(supervisor (Scrooge Eben) (Warbucks Oliver))

(address (Cratchet Robert) 
         (Allston (N Harvard Street) 16))
(job (Cratchet Robert) (accounting scrivener))
(salary (Cratchet Robert) 18000)
(supervisor (Cratchet Robert) (Scrooge Eben))

Mae yna hefyd ysgrifennydd i'r pennaeth mawr:

(address (Aull DeWitt) 
         (Slumerville (Onion Square) 5))
(job (Aull DeWitt) (administration secretary))
(salary (Aull DeWitt) 25000)
(supervisor (Aull DeWitt) (Warbucks Oliver))

Mae'r gronfa ddata hefyd yn cynnwys haeriadau am ba fathau o swyddi y gellir eu gwneud gan bobl sy'n dal mathau eraill o swyddi. Er enghraifft, gall dewin cyfrifiaduron wneud swyddi rhaglennydd cyfrifiaduron a thechnegydd cyfrifiaduron:

(can-do-job (computer wizard) 
            (computer programmer))

(can-do-job (computer wizard) 
            (computer technician))

Gallai rhaglennydd cyfrifiaduron lenwi bwlch hyfforddai:

(can-do-job (computer programmer)
            (computer programmer trainee))

Hefyd, fel sy'n hysbys iawn,

(can-do-job (administration secretary)
            (administration big wheel))

Ymholiadau syml

Mae'r iaith ymholi'n caniatáu i ddefnyddwyr adalw gwybodaeth o'r gronfa ddata drwy gyflwyno ymholiadau mewn ymateb i anogiad y system. Er enghraifft, i ganfod pob rhaglennydd cyfrifiaduron gellir dweud

;;; Query input:
(job ?x (computer programmer))

Bydd y system yn ymateb gyda'r eitemau canlynol:

;;; Query results:
(job (Hacker Alyssa P) (computer programmer))
(job (Fect Cy D) (computer programmer))

Mae'r ymholiad mewnbwn yn pennu ein bod yn chwilio am gofnodion yn y gronfa ddata sy'n cyfateb i batrwm penodol. Yn yr enghraifft hon, mae'r patrwm yn pennu cofnodion sy'n cynnwys tair eitem, a'r gyntaf yw'r symbol llythrennol job, gall yr ail fod yn unrhyw beth, a'r drydedd yw'r rhestr lythrennol (computer programmer). Pennir yr “unrhyw beth” a all fod yn ail eitem y rhestr sy'n cyfateb gan newidyn patrwm, ?x. Ffurf gyffredinol newidyn patrwm yw symbol, a gymerir yn enw'r newidyn, ag arwydd cwestiwn o'i flaen. Fe welwn isod pam mae'n ddefnyddiol pennu enwau ar gyfer newidynnau patrwm yn hytrach na rhoi ? mewn patrymau yn unig i gynrychioli “unrhyw beth.” Mae'r system yn ymateb i ymholiad syml drwy ddangos pob cofnod yn y gronfa ddata sy'n cyfateb i'r patrwm penodedig.

Gall patrwm gael mwy nag un newidyn. Er enghraifft, bydd yr ymholiad

(address ?x ?y)

yn rhestru cyfeiriadau'r holl gyflogeion.

Gall patrwm fod heb newidynnau; yn yr achos hwnnw, dim ond penderfynu a yw'r patrwm hwnnw'n gofnod yn y gronfa ddata y mae'r ymholiad. Os ydyw, bydd un cyfatebiad; os nad ydyw, ni fydd cyfatebiadau.

Gall yr un newidyn patrwm ymddangos fwy nag unwaith mewn ymholiad, gan bennu bod rhaid i'r un “unrhyw beth” ymddangos ym mhob safle. Dyma pam mae gan newidynnau enwau. Er enghraifft, mae

(supervisor ?x ?x)

yn canfod yr holl bobl sy'n goruchwylio eu hunain (er nad oes haeriadau o'r fath yn ein cronfa ddata enghreifftiol).

Mae'r ymholiad

(job ?x (computer ?type))

yn cyfateb i bob cofnod swydd y mae ei drydedd eitem yn rhestr ddwy elfen y mae ei heitem gyntaf yn computer:

(job (Bitdiddle Ben) (computer wizard))
(job (Hacker Alyssa P) (computer programmer))
(job (Fect Cy D) (computer programmer))
(job (Tweakit Lem E) (computer technician))

Nid yw'r un patrwm hwn yn cyfateb i

(job (Reasoner Louis) 
     (computer programmer trainee))

oherwydd mae trydedd eitem y cofnod yn rhestr o dair elfen, ac mae trydedd eitem y patrwm yn pennu y dylai fod dwy elfen. Pe baem am newid y patrwm fel y gallai'r drydedd eitem fod yn unrhyw restr sy'n dechrau ag computer, gallem bennu²⁶⁶

(job ?x (computer . ?type))

Er enghraifft, mae

(computer . ?type)

yn cyfateb i'r data

(computer programmer trainee)

gydag ?type yn rhestr (programmer trainee). Mae hefyd yn cyfateb i'r data

(computer programmer)

gydag ?type yn rhestr (programmer), ac yn cyfateb i'r data

(computer)

gydag ?type yn rhestr wag ().

Gallwn ddisgrifio prosesu ymholiadau syml gan yr iaith ymholi fel a ganlyn:

Mae'r system yn canfod pob aseiniad i newidynnau ym mhatrwm yr ymholiad sy'n bodloni'r patrwm—hynny yw, pob set o werthoedd ar gyfer y newidynnau fel bod y canlyniad yn y gronfa ddata os yw newidynnau'r patrwm wedi'u henghreifftio â'r gwerthoedd (wedi'u disodli ganddynt).
Mae'r system yn ymateb i'r ymholiad drwy restru pob enghreifftiad o batrwm yr ymholiad gyda'r aseiniadau newidynnau sy'n ei fodloni.

Sylwch, os nad oes gan y patrwm newidynnau, fod yr ymholiad yn lleihau i benderfynu a yw'r patrwm hwnnw yn y gronfa ddata. Os ydyw, mae'r aseiniad gwag, nad yw'n aseinio gwerthoedd i newidynnau, yn bodloni'r patrwm hwnnw ar gyfer y gronfa ddata honno.

Ymarfer 4.55: Rhowch ymholiadau syml sy'n adalw'r wybodaeth ganlynol o'r gronfa ddata:

yr holl bobl a oruchwylir gan Ben Bitdiddle;
enwau a swyddi'r holl bobl yn yr adran gyfrifyddu;
enwau a chyfeiriadau'r holl bobl sy'n byw yn Slumerville.

Ymholiadau cyfansawdd

Ymholiadau syml yw gweithrediadau cyntefig yr iaith ymholi. Er mwyn ffurfio gweithrediadau cyfansawdd, mae'r iaith ymholi'n darparu dulliau cyfuno. Un peth sy'n gwneud yr iaith ymholi'n iaith raglennu resymegol yw bod y dulliau cyfuno'n adlewyrchu'r dulliau cyfuno a ddefnyddir i ffurfio mynegiadau rhesymegol: and, or, ac not. (Yma nid gweithdrefnau cyntefig Lisp yw and, or, ac not, ond yn hytrach weithrediadau sydd wedi'u hymgorffori yn yr iaith ymholi.)

Gallwn ddefnyddio and fel a ganlyn i ganfod cyfeiriadau'r holl raglenwyr cyfrifiaduron:

(and (job ?person (computer programmer))
     (address ?person ?where))

Yr allbwn sy'n deillio o hyn yw

(and (job (Hacker Alyssa P) 
          (computer programmer))
     (address (Hacker Alyssa P) 
              (Cambridge (Mass Ave) 78)))

(and (job (Fect Cy D) (computer programmer))
     (address (Fect Cy D) 
              (Cambridge (Ames Street) 3)))

Yn gyffredinol, mae

(and ⟨query₁⟩ ⟨query₂⟩ … ⟨queryₙ⟩)

yn cael ei fodloni gan bob set o werthoedd ar gyfer y newidynnau patrwm sy'n bodloni $⟨ q u e r y_{1} ⟩$ … $⟨ q u e r y_{n} ⟩$ ar yr un pryd.

Fel gydag ymholiadau syml, mae'r system yn prosesu ymholiad cyfansawdd drwy ganfod pob aseiniad i'r newidynnau patrwm sy'n bodloni'r ymholiad, ac yna'n dangos enghreifftiadau o'r ymholiad gyda'r gwerthoedd hynny.

Dull arall o adeiladu ymholiadau cyfansawdd yw drwy or. Er enghraifft, bydd

(or (supervisor ?x (Bitdiddle Ben))
    (supervisor ?x (Hacker Alyssa P)))

yn canfod yr holl gyflogeion a oruchwylir gan Ben Bitdiddle neu Alyssa P. Hacker:

(or (supervisor (Hacker Alyssa P) 
                (Bitdiddle Ben))
    (supervisor (Hacker Alyssa P) 
                (Hacker Alyssa P)))

(or (supervisor (Fect Cy D) 
                (Bitdiddle Ben))
    (supervisor (Fect Cy D) 
                (Hacker Alyssa P)))

(or (supervisor (Tweakit Lem E) 
                (Bitdiddle Ben))
    (supervisor (Tweakit Lem E) 
                (Hacker Alyssa P)))

(or (supervisor (Reasoner Louis) 
                (Bitdiddle Ben))
    (supervisor (Reasoner Louis) 
                (Hacker Alyssa P)))

Yn gyffredinol, mae

(or ⟨query₁⟩ ⟨query₂⟩ … ⟨queryₙ⟩)

yn cael ei fodloni gan bob set o werthoedd ar gyfer y newidynnau patrwm sy'n bodloni o leiaf un o $⟨ q u e r y_{1} ⟩$ … $⟨ q u e r y_{n} ⟩$ .

Gellir ffurfio ymholiadau cyfansawdd hefyd gydag not. Er enghraifft, mae

(and (supervisor ?x (Bitdiddle Ben))
     (not (job ?x (computer programmer))))

yn canfod yr holl bobl a oruchwylir gan Ben Bitdiddle nad ydynt yn rhaglenwyr cyfrifiaduron. Yn gyffredinol, mae

(not ⟨query₁⟩)

yn cael ei fodloni gan bob aseiniad i'r newidynnau patrwm nad yw'n bodloni $⟨ q u e r y_{1} ⟩$ .²⁶⁷

Gelwir y ffurf gyfuno olaf yn lisp-value. Pan mai lisp-value yw elfen gyntaf patrwm, mae'n pennu bod yr elfen nesaf yn draethiad Lisp i'w gymhwyso i weddill yr elfennau (wedi'u henghreifftio) fel argiau. Yn gyffredinol, bydd

(lisp-value ⟨predicate⟩ ⟨arg₁⟩ … ⟨argₙ⟩)

yn cael ei fodloni gan aseiniadau i'r newidynnau patrwm y mae'r ⟨predicate⟩ wedi'i gymhwyso i'r $⟨ a r g_{1} ⟩$ … $⟨ a r g_{n} ⟩$ wedi'u henghreifftio yn wir ar eu cyfer. Er enghraifft, i ganfod yr holl bobl y mae eu cyflog yn fwy na $30,000, gallem ysgrifennu²⁶⁸

(and (salary ?person ?amount)
     (lisp-value > ?amount 30000))

Ymarfer 4.56: Lluniwch ymholiadau cyfansawdd sy'n adalw'r wybodaeth ganlynol:

enwau'r holl bobl a oruchwylir gan Ben Bitdiddle, ynghyd â'u cyfeiriadau;
yr holl bobl y mae eu cyflog yn llai na chyflog Ben Bitdiddle, ynghyd â'u cyflog a chyflog Ben Bitdiddle;
yr holl bobl a oruchwylir gan rywun nad yw yn yr adran gyfrifiaduron, ynghyd ag enw a swydd y goruchwyliwr.

Rheolau

Yn ogystal ag ymholiadau cyntefig ac ymholiadau cyfansawdd, mae'r iaith ymholi'n darparu dulliau ar gyfer haniaethu ymholiadau. Darperir y rhain gan reolau. Mae'r rheol

(rule (lives-near ?person-1 ?person-2)
      (and (address ?person-1 
                    (?town . ?rest-1))
           (address ?person-2 
                    (?town . ?rest-2))
           (not (same ?person-1 ?person-2))))

yn pennu bod dau berson yn byw'n agos at ei gilydd os ydynt yn byw yn yr un dref. Mae'r cymal not olaf yn atal y rheol rhag dweud bod pawb yn byw'n agos atynt eu hunain. Diffinnir y berthynas same gan reol syml iawn:²⁶⁹

(rule (same ?x ?x))

Mae'r rheol ganlynol yn datgan bod person yn “bennaeth” mewn sefydliad os yw'n goruchwylio rhywun sydd yn ei dro yn oruchwyliwr:

(rule (wheel ?person)
      (and (supervisor ?middle-manager 
                       ?person)
           (supervisor ?x ?middle-manager)))

Ffurf gyffredinol rheol yw

(rule ⟨conclusion⟩ ⟨body⟩)

lle mae ⟨conclusion⟩ yn batrwm a lle mae ⟨body⟩ yn unrhyw ymholiad.²⁷⁰ Gallwn feddwl am reol fel pe bai'n cynrychioli set fawr (hyd yn oed anfeidraidd) o haeriadau, sef pob enghreifftiad o gasgliad y rheol gydag aseiniadau newidynnau sy'n bodloni corff y rheol. Pan ddisgrifiwyd ymholiadau syml (patrymau), dywedasom fod aseiniad i newidynnau yn bodloni patrwm os yw'r patrwm wedi'i enghreifftio yn y gronfa ddata. Ond nid oes angen i'r patrwm fod yn benodol yn y gronfa ddata fel haeriad. Gall fod yn haeriad ymhlyg a awgrymir gan reol. Er enghraifft, mae'r ymholiad

(lives-near ?x (Bitdiddle Ben))

yn arwain at

(lives-near (Reasoner Louis) (Bitdiddle Ben))
(lives-near (Aull DeWitt) (Bitdiddle Ben))

I ganfod yr holl raglenwyr cyfrifiaduron sy'n byw'n agos at Ben Bitdiddle, gallwn ofyn

(and (job ?x (computer programmer))
     (lives-near ?x (Bitdiddle Ben)))

Fel yn achos gweithdrefnau cyfansawdd, gellir defnyddio rheolau fel rhannau o reolau eraill (fel y gwelsom gyda'r rheol lives-near uchod) neu hyd yn oed eu diffinio'n ddychweliadol. Er enghraifft, mae'r rheol

(rule (outranked-by ?staff-person ?boss)
      (or (supervisor ?staff-person ?boss)
          (and (supervisor ?staff-person 
                           ?middle-manager)
               (outranked-by ?middle-manager 
                             ?boss))))

yn dweud bod aelod staff yn is na phennaeth yn hierarchaeth y sefydliad os yw'r pennaeth yn oruchwyliwr y person neu (yn ddychweliadol) os yw goruchwyliwr y person yn is na'r pennaeth.

Ymarfer 4.57: Diffiniwch reol sy'n dweud y gall person 1 gymryd lle person 2 os yw naill ai person 1 yn gwneud yr un swydd â pherson 2 neu os gall rhywun sy'n gwneud swydd person 1 hefyd wneud swydd person 2, ac os nad yw person 1 a pherson 2 yr un person. Gan ddefnyddio eich rheol, rhowch ymholiadau sy'n canfod y canlynol:

yr holl bobl a all gymryd lle Cy D. Fect;
yr holl bobl a all gymryd lle rhywun sy'n cael mwy o gyflog na hwy, ynghyd â'r ddau gyflog.

Ymarfer 4.58: Diffiniwch reol sy'n dweud bod person yn “bennaeth mawr” mewn adran os yw'r person yn gweithio yn yr adran ond heb oruchwyliwr sy'n gweithio yn yr adran.

Ymarfer 4.59: Mae Ben Bitdiddle wedi methu un cyfarfod yn ormod. Gan ofni y gallai ei arfer o anghofio cyfarfodydd gostio'i swydd iddo, mae Ben yn penderfynu gwneud rhywbeth am y peth. Mae'n ychwanegu holl gyfarfodydd wythnosol y cwmni at gronfa ddata Microshaft drwy haeru'r canlynol:
(meeting accounting (Monday 9am))
(meeting administration (Monday 10am))
(meeting computer (Wednesday 3pm))
(meeting administration (Friday 1pm))
Mae pob un o'r haeriadau uchod ar gyfer cyfarfod adran gyfan. Mae Ben hefyd yn ychwanegu cofnod ar gyfer y cyfarfod cwmni cyfan sy'n cwmpasu pob adran. Mae holl gyflogeion y cwmni'n mynychu'r cyfarfod hwn.
(meeting whole-company (Wednesday 4pm))
Fore Gwener, mae Ben am holi'r gronfa ddata am yr holl gyfarfodydd sy'n digwydd y diwrnod hwnnw. Pa ymholiad dylai ei ddefnyddio?
Nid yw Alyssa P. Hacker wedi'i phlesio. Mae hi o'r farn y byddai'n llawer mwy defnyddiol gallu gofyn am ei chyfarfodydd drwy bennu ei henw. Felly mae'n dylunio rheol sy'n dweud bod cyfarfodydd person yn cynnwys pob cyfarfod whole-company ynghyd â phob cyfarfod adran y person hwnnw. Llanwch gorff rheol Alyssa.
(rule (meeting-time ?person ?day-and-time)
      ⟨rule-body⟩)
Mae Alyssa'n cyrraedd y gwaith fore Mercher ac yn pendroni pa gyfarfodydd y mae'n rhaid iddi eu mynychu y diwrnod hwnnw. Ar ôl diffinio'r rheol uchod, pa ymholiad dylai ei wneud i ganfod hyn?

Ymarfer 4.60: Drwy roi'r ymholiad
(lives-near ?person (Hacker Alyssa P))
gall Alyssa P. Hacker ganfod pobl sy'n byw'n agos ati, y gall deithio i'r gwaith gyda hwy. Ar y llaw arall, pan geisia ganfod pob pâr o bobl sy'n byw'n agos at ei gilydd drwy holi
(lives-near ?person-1 ?person-2)
mae'n sylwi bod pob pâr o bobl sy'n byw'n agos at ei gilydd wedi'i restru ddwywaith; er enghraifft,
(lives-near (Hacker Alyssa P) (Fect Cy D))
(lives-near (Fect Cy D) (Hacker Alyssa P))
Pam mae hyn yn digwydd? A oes ffordd o ganfod rhestr o bobl sy'n byw'n agos at ei gilydd, lle mae pob pâr yn ymddangos unwaith yn unig? Eglurwch.

Rhesymeg fel rhaglenni

Gallwn ystyried rheol yn fath o oblygiad rhesymegol: Os yw aseiniad o werthoedd i newidynnau patrwm yn bodloni'r corff, yna mae'n bodloni'r casgliad. O ganlyniad, gallwn ystyried bod gan yr iaith ymholi'r gallu i gyflawni diddwythiadau rhesymegol ar sail y rheolau. Er enghraifft, ystyriwch y gweithrediad append a ddisgrifir ar ddechrau 4.4. Fel y dywedasom, gellir nodweddu append gan y ddwy reol ganlynol:

Ar gyfer unrhyw restr y, mae'r rhestr wag ac y yn cyfuno drwy append i ffurfio y.
Ar gyfer unrhyw u, v, y, ac z, mae (cons u v) ac y yn cyfuno drwy append i ffurfio (cons u z) os yw v ac y yn cyfuno drwy append i ffurfio z.

I fynegi hyn yn ein hiaith ymholi, diffiniwn ddwy reol ar gyfer perthynas

(append-to-form x y z)

y gallwn ei dehongli i olygu “mae x ac y yn cyfuno drwy append i ffurfio z”:

(rule (append-to-form () ?y ?y))
(rule (append-to-form (?u . ?v) ?y (?u . ?z))
      (append-to-form ?v ?y ?z))

Nid oes corff gan y rheol gyntaf, sy'n golygu bod y casgliad yn dal ar gyfer unrhyw werth ?y. Sylwch sut mae'r ail reol yn defnyddio nodiant cynffon ddotiog i enwi car ac cdr rhestr.

O gael y ddwy reol hyn, gallwn lunio ymholiadau sy'n cyfrifo append dwy restr:

;;; Query input:
(append-to-form (a b) (c d) ?z)

;;; Query results:
(append-to-form (a b) (c d) (a b c d))

Yn fwy trawiadol, gallwn ddefnyddio'r un rheolau i ofyn y cwestiwn “Pa restr sy'n rhoi (a b c d) pan gaiff ei chyfuno drwy append ag (a b)?” Gwneir hyn fel a ganlyn:

;;; Query input:
(append-to-form (a b) ?y (a b c d))

;;; Query results:
(append-to-form (a b) (c d) (a b c d))

Gallwn hefyd ofyn am bob pâr o restrau sy'n cyfuno drwy append i ffurfio (a b c d):

;;; Query input:
(append-to-form ?x ?y (a b c d))

;;; Query results:
(append-to-form () (a b c d) (a b c d))
(append-to-form (a) (b c d) (a b c d))
(append-to-form (a b) (c d) (a b c d))
(append-to-form (a b c) (d) (a b c d))
(append-to-form (a b c d) () (a b c d))

Gall y system ymholi ymddangos fel pe bai'n dangos cryn dipyn o ddeallusrwydd wrth ddefnyddio'r rheolau i ddiddwytho'r atebion i'r ymholiadau uchod. Mewn gwirionedd, fel y gwelwn yn yr adran nesaf, mae'r system yn dilyn algorithm penodol wrth ddadblethu'r rheolau. Yn anffodus, er bod y system yn gweithio'n drawiadol yn achos append, gall y dulliau cyffredinol fethu mewn achosion mwy cymhleth, fel y gwelwn yn 4.4.3.

Ymarfer 4.61: Mae'r rheolau canlynol yn gweithredu perthynas next-to sy'n canfod elfennau cyfagos rhestr:
(rule (?x next-to ?y in (?x ?y . ?u)))
(rule (?x next-to ?y in (?v . ?z))
      (?x next-to ?y in ?z))
Beth fydd yr ymateb i'r ymholiadau canlynol?
(?x next-to ?y in (1 (2 3) 4))
(?x next-to 1 in (2 1 3 1))

Ymarfer 4.62: Diffiniwch reolau i weithredu gweithrediad last-pair Ymarfer 2.17, sy'n dychwelyd rhestr sy'n cynnwys elfen olaf rhestr ddiwag. Gwiriwch eich rheolau ar ymholiadau megis (last-pair (3) ?x), (last-pair (1 2 3) ?x) ac (last-pair (2 ?x) (3)). A yw eich rheolau'n gweithio'n gywir ar ymholiadau megis (last-pair ?x (3))?

Ymarfer 4.63: Mae'r gronfa ddata ganlynol (gweler Genesis 4) yn olrhain achau disgynyddion Ada yn ôl i Adam, drwy Cain:
(son Adam Cain) (son Cain Enoch)
(son Enoch Irad) (son Irad Mehujael)
(son Mehujael Methushael)
(son Methushael Lamech)
(wife Lamech Ada) (son Ada Jabal)
(son Ada Jubal)
Lluniwch reolau megis “Os yw $S$ yn fab i $f$ , ac os yw $f$ yn fab i $G$ , yna mae $S$ yn ŵyr i $G$ ” ac “Os yw $W$ yn wraig i $M$ , ac os yw $S$ yn fab i $W$ , yna mae $S$ yn fab i $M$ ” (a oedd, yn ôl pob tebyg, yn fwy gwir yn oes y Beibl nag ydyw heddiw) a fydd yn galluogi'r system ymholi i ganfod ŵyr Cain; meibion Lamech; wyrion Methushael. (Gweler Ymarfer 4.69 am rai rheolau i ddiddwytho perthnasoedd mwy cymhleth.)

4.4.2Sut Mae'r System Ymholi'n Gweithio

Yn adran 4.4.4 byddwn yn cyflwyno gweithrediad y dehonglydd ymholi fel casgliad o weithdrefnau. Yn yr adran hon rhown drosolwg sy'n egluro strwythur cyffredinol y system yn annibynnol ar fanylion gweithredu lefel isel. Ar ôl disgrifio gweithrediad y dehonglydd, byddwn mewn sefyllfa i ddeall rhai o'i gyfyngiadau a rhai o'r ffyrdd cynnil y mae gweithrediadau rhesymegol yr iaith ymholi'n wahanol i weithrediadau rhesymeg fathemategol.

Dylai fod yn amlwg bod rhaid i'r gwerthusydd ymholi gyflawni rhyw fath o chwilio er mwyn paru ymholiadau â ffeithiau a rheolau yn y gronfa ddata. Un ffordd o wneud hyn fyddai gweithredu'r system ymholi fel rhaglen an-benderfyniaethol, gan ddefnyddio gwerthusydd amb 4.3 (gweler Ymarfer 4.78). Posibilrwydd arall yw rheoli'r chwilio gyda chymorth ffrydiau. Mae ein gweithrediad yn dilyn yr ail ddull hwn.

Mae'r system ymholi wedi'i threfnu o amgylch dau weithrediad canolog a elwir yn baru patrymau ac uno patrymau. Yn gyntaf disgrifiwn baru patrymau ac eglurwn sut mae'r gweithrediad hwn, ynghyd â threfnu gwybodaeth yn nhermau ffrydiau o fframiau, yn ein galluogi i weithredu ymholiadau syml a chyfansawdd. Yna trafodwn uno patrymau, cyffredinoliad o baru patrymau sydd ei angen i weithredu rheolau. Yn olaf, dangoswn sut mae'r dehonglydd ymholi cyfan yn cyd-fynd drwy weithdrefn sy'n dosbarthu mynegiadau mewn modd sy'n cyfateb i'r ffordd y mae eval yn dosbarthu mynegiadau ar gyfer y dehonglydd a ddisgrifir yn 4.1.

Paru patrymau

Rhaglen yw parwr patrymau sy'n profi a yw eitem ddata yn cyfateb i batrwm penodedig. Er enghraifft, mae'r rhestr ddata ((a b) c (a b)) yn cyfateb i'r patrwm (?x c ?x) gyda'r newidyn patrwm ?x wedi'i rwymo i (a b). Mae'r un rhestr ddata'n cyfateb i'r patrwm (?x ?y ?z) gydag ?x ac ?z ill dau wedi'u rhwymo i (a b) ac ?y wedi'i rwymo i c. Mae hefyd yn cyfateb i'r patrwm ((?x ?y) c (?x ?y)) gydag ?x wedi'i rwymo i a ac ?y wedi'i rwymo i b. Fodd bynnag, nid yw'n cyfateb i'r patrwm (?x a ?y), gan fod y patrwm hwnnw'n pennu rhestr y mae ei hail elfen yn symbol a.

Mae'r parwr patrymau a ddefnyddir gan y system ymholi yn cymryd fel mewnbynnau batrwm, eitem ddata, a ffrâm sy'n pennu rhwymiadau ar gyfer amrywiol newidynnau patrwm. Mae'n gwirio a yw'r eitem ddata'n cyfateb i'r patrwm mewn ffordd sy'n gyson â'r rhwymiadau sydd eisoes yn y ffrâm. Os felly, mae'n dychwelyd y ffrâm a roddwyd wedi'i hategu gan unrhyw rwymiadau a allai fod wedi'u pennu gan y cyfatebiad. Fel arall, mae'n nodi bod y paru wedi methu.

Er enghraifft, bydd defnyddio'r patrwm (?x ?y ?x) i baru ag (a b a) o gael ffrâm wag yn dychwelyd ffrâm sy'n pennu bod ?x wedi'i rwymo i a a bod ?y wedi'i rwymo i b. Bydd ceisio paru gyda'r un patrwm, yr un eitem ddata, a ffrâm sy'n pennu bod ?y wedi'i rwymo i a yn methu. Bydd ceisio paru gyda'r un patrwm, yr un eitem ddata, a ffrâm lle mae ?y wedi'i rwymo i b ac ?x heb ei rwymo yn dychwelyd y ffrâm a roddwyd wedi'i hategu gan rwymiad ?x i a.

Y parwr patrymau yw'r unig fecanwaith sydd ei angen i brosesu ymholiadau syml nad ydynt yn cynnwys rheolau. Er enghraifft, i brosesu'r ymholiad

(job ?x (computer programmer))

sganiwn drwy bob haeriad yn y gronfa ddata a detholwn y rhai sy'n cyfateb i'r patrwm mewn perthynas â ffrâm sy'n wag i ddechrau. Ar gyfer pob cyfatebiad a ganfyddwn, defnyddiwn y ffrâm a ddychwelir gan y paru i enghreifftio'r patrwm â gwerth ar gyfer ?x.

Ffrydiau o fframiau

Trefnir profi patrymau mewn perthynas â fframiau drwy ddefnyddio ffrydiau. O gael un ffrâm, mae'r broses baru'n mynd drwy gofnodion y gronfa ddata fesul un. Ar gyfer pob cofnod, mae'r parwr yn cynhyrchu naill ai symbol arbennig sy'n nodi bod y paru wedi methu neu estyniad i'r ffrâm. Cesglir canlyniadau holl gofnodion y gronfa ddata mewn ffrwd, a basir drwy hidlydd i dynnu'r methiannau. Y canlyniad yw ffrwd o'r holl fframiau sy'n ymestyn y ffrâm a roddwyd drwy baru â rhyw haeriad yn y gronfa ddata.²⁷¹

Yn ein system, mae ymholiad yn cymryd ffrwd fewnbwn o fframiau ac yn cyflawni'r gweithrediad paru uchod ar gyfer pob ffrâm yn y ffrwd, fel y dangosir yn Ffigur 4.4. Hynny yw, ar gyfer pob ffrâm yn y ffrwd fewnbwn, mae'r ymholiad yn cynhyrchu ffrwd newydd sy'n cynnwys pob estyniad i'r ffrâm honno drwy baru â haeriadau yn y gronfa ddata. Cyfunir yr holl ffrydiau hyn wedyn i ffurfio un ffrwd anferth, sy'n cynnwys pob estyniad posibl i bob ffrâm yn y ffrwd fewnbwn. Y ffrwd hon yw allbwn yr ymholiad.

Ffigur 4.4: Mae ymholiad yn prosesu ffrwd o fframiau.

I ateb ymholiad syml, defnyddiwn yr ymholiad gyda ffrwd fewnbwn sy'n cynnwys un ffrâm wag. Mae'r ffrwd allbwn sy'n deillio o hyn yn cynnwys pob estyniad i'r ffrâm wag (hynny yw, pob ateb i'n hymholiad). Defnyddir y ffrwd hon o fframiau wedyn i gynhyrchu ffrwd o gopïau o batrwm gwreiddiol yr ymholiad gyda'r newidynnau wedi'u henghreifftio â'r gwerthoedd ym mhob ffrâm, a dyma'r ffrwd a argreffir yn y pen draw.

Ymholiadau cyfansawdd

Daw gwir geinder y gweithrediad ffrydiau o fframiau i'r amlwg pan ymdriniwn ag ymholiadau cyfansawdd. Mae prosesu ymholiadau cyfansawdd yn defnyddio gallu ein parwr i fynnu bod cyfatebiad yn gyson â ffrâm benodedig. Er enghraifft, i ymdrin ag and dau ymholiad, megis

(and (can-do-job 
      ?x 
      (computer programmer trainee))
     (job ?person ?x))

(yn anffurfiol, “Darganfyddwch yr holl bobl a all wneud swydd rhaglennydd cyfrifiaduron dan hyfforddiant”), yn gyntaf canfyddwn bob cofnod sy'n cyfateb i'r patrwm

(can-do-job ?x (computer programmer trainee))

Mae hyn yn cynhyrchu ffrwd o fframiau, pob un yn cynnwys rhwymiad ar gyfer ?x. Yna ar gyfer pob ffrâm yn y ffrwd canfyddwn bob cofnod sy'n cyfateb i

(job ?person ?x)

mewn ffordd sy'n gyson â'r rhwymiad a roddwyd ar gyfer ?x. Bydd pob cyfatebiad o'r fath yn cynhyrchu ffrâm sy'n cynnwys rhwymiadau ar gyfer ?x ac ?person. Gellir gweld and dau ymholiad fel cyfuniad mewn cyfres o'r ddau ymholiad cyfansoddol, fel y dangosir yn Ffigur 4.5. Mae'r fframiau sy'n pasio drwy hidlydd yr ymholiad cyntaf yn cael eu hidlo a'u hymestyn ymhellach gan yr ail ymholiad.

Ffigur 4.5: Cynhyrchir cyfuniad and dau ymholiad drwy weithredu ar y ffrwd o fframiau mewn cyfres.

Mae Ffigur 4.6 yn dangos y dull cyfatebol ar gyfer cyfrifo or dau ymholiad fel cyfuniad paralel o'r ddau ymholiad cyfansoddol. Estynnir y ffrwd fewnbwn o fframiau ar wahân gan bob ymholiad. Yna cyfunir y ddwy ffrwd sy'n deillio o hynny i gynhyrchu'r ffrwd allbwn derfynol.

Ffigur 4.6: Cynhyrchir cyfuniad or dau ymholiad drwy weithredu ar y ffrwd o fframiau'n baralel a chyfuno'r canlyniadau.

Hyd yn oed o'r disgrifiad lefel uchel hwn, mae'n amlwg y gall prosesu ymholiadau cyfansawdd fod yn araf. Er enghraifft, gan y gall ymholiad gynhyrchu mwy nag un ffrâm allbwn ar gyfer pob ffrâm fewnbwn, a bod pob ymholiad mewn and yn cael ei fframiau mewnbwn o'r ymholiad blaenorol, gallai ymholiad and, yn yr achos gwaethaf, orfod cyflawni nifer o bariadau sy'n esbonyddol yn nifer yr ymholiadau (gweler Ymarfer 4.76).²⁷² Er bod systemau ar gyfer ymdrin ag ymholiadau syml yn unig yn eithaf ymarferol, mae ymdrin ag ymholiadau cymhleth yn eithriadol o anodd.²⁷³

O safbwynt ffrydiau o fframiau, mae not rhyw ymholiad yn gweithredu fel hidlydd sy'n tynnu pob ffrâm y gellir bodloni'r ymholiad ar ei chyfer. Er enghraifft, o gael y patrwm

(not (job ?x (computer programmer)))

ceisiwn, ar gyfer pob ffrâm yn y ffrwd fewnbwn, gynhyrchu fframiau estyniad sy'n bodloni (job ?x (computer programmer)). Tynnwn o'r ffrwd fewnbwn bob ffrâm y mae estyniadau o'r fath yn bodoli ar ei chyfer. Y canlyniad yw ffrwd sy'n cynnwys dim ond y fframiau hynny lle nad yw'r rhwymiad ar gyfer ?x yn bodloni (job ?x (computer programmer)). Er enghraifft, wrth brosesu'r ymholiad

(and (supervisor ?x ?y)
     (not (job ?x (computer programmer))))

bydd y cymal cyntaf yn cynhyrchu fframiau â rhwymiadau ar gyfer ?x ac ?y. Bydd y cymal not wedyn yn hidlo'r rhain drwy dynnu pob ffrâm lle mae'r rhwymiad ar gyfer ?x yn bodloni'r cyfyngiad bod ?x yn rhaglennydd cyfrifiaduron.²⁷⁴

Gweithredir y ffurf arbennig lisp-value fel hidlydd tebyg ar ffrydiau o fframiau. Defnyddiwn bob ffrâm yn y ffrwd i enghreifftio unrhyw newidynnau yn y patrwm, ac yna cymhwyswn draethiad Lisp. Tynnwn o'r ffrwd fewnbwn bob ffrâm y mae'r traethiad yn methu ar ei chyfer.

Uno patrymau

Er mwyn ymdrin â rheolau yn yr iaith ymholi, rhaid inni allu canfod y rheolau y mae eu casgliadau'n cyfateb i batrwm ymholiad penodol. Mae casgliadau rheolau'n debyg i haeriadau ac eithrio y gallant gynnwys newidynnau, felly bydd angen cyffredinoliad o baru patrymau arnom—a elwir yn uno patrymau—lle gall y “patrwm” a'r “eitem ddata” ill dau gynnwys newidynnau.

Mae unydd yn cymryd dau batrwm, pob un yn cynnwys cysonion a newidynnau, ac yn penderfynu a yw'n bosibl aseinio gwerthoedd i'r newidynnau a fydd yn gwneud y ddau batrwm yn hafal. Os felly, mae'n dychwelyd ffrâm sy'n cynnwys y rhwymiadau hyn. Er enghraifft, bydd uno (?x a ?y) ac (?y ?z a) yn pennu ffrâm lle mae'n rhaid i ?x, ?y, ac ?z i gyd gael eu rhwymo i a. Ar y llaw arall, bydd uno (?x ?y a) ac (?x b ?y) yn methu, oherwydd nid oes gwerth ar gyfer ?y a all wneud y ddau batrwm yn hafal. (Er mwyn i ail elfennau'r patrymau fod yn hafal, byddai'n rhaid i ?y fod yn b; fodd bynnag, er mwyn i'r trydydd elfennau fod yn hafal, byddai'n rhaid i ?y fod yn a.) Mae'r unydd a ddefnyddir yn y system ymholi, fel y parwr patrymau, yn cymryd ffrâm fel mewnbwn ac yn cyflawni uno sy'n gyson â'r ffrâm hon.

Yr algorithm uno yw'r rhan fwyaf anodd yn dechnegol o'r system ymholi. Gyda phatrymau cymhleth, gall uno ymddangos fel pe bai angen diddwytho. I uno (?x ?x) ac ((a ?y c) (a b ?z)), er enghraifft, rhaid i'r algorithm gasglu y dylai ?x fod yn (a b c), y dylai ?y fod yn b, ac y dylai ?z fod yn c. Gallwn feddwl am y broses hon fel datrys set o hafaliadau rhwng cydrannau'r patrymau. Yn gyffredinol, hafaliadau cydamserol yw'r rhain, a gall fod angen cryn dipyn o drin i'w datrys.²⁷⁵ Er enghraifft, gellir meddwl am uno (?x ?x) ac ((a ?y c) (a b ?z)) fel pennu'r hafaliadau cydamserol

?x = (a ?y c)
?x = (a b ?z)

Mae'r hafaliadau hyn yn awgrymu bod

(a ?y c) = (a b ?z)

sydd yn ei dro yn awgrymu bod

a = a, ?y = b, c = ?z,

ac felly fod

?x = (a b c)

Mewn paru patrymau llwyddiannus, mae holl newidynnau'r patrwm yn cael eu rhwymo, a dim ond cysonion sydd yn y gwerthoedd y cânt eu rhwymo iddynt. Mae hyn hefyd yn wir am yr holl enghreifftiau o uno a welsom hyd yma. Yn gyffredinol, fodd bynnag, efallai na fydd uno llwyddiannus yn pennu gwerthoedd y newidynnau'n llwyr; gall rhai newidynnau aros heb eu rhwymo a gall eraill gael eu rhwymo i werthoedd sy'n cynnwys newidynnau.

Ystyriwch uno (?x a) ac ((b ?y) ?z). Gallwn ddiddwytho bod ?x = (b ?y) ac a = ?z, ond ni allwn ddatrys ymhellach am ?x nac ?y. Nid yw'r uno'n methu, gan ei bod yn sicr yn bosibl gwneud y ddau batrwm yn hafal drwy aseinio gwerthoedd i ?x ac ?y. Gan nad yw'r cyfatebiad hwn yn cyfyngu mewn unrhyw ffordd ar y gwerthoedd y gall ?y eu cymryd, ni roddir rhwymiad ar gyfer ?y yn y ffrâm ganlyniad. Mae'r cyfatebiad, fodd bynnag, yn cyfyngu ar werth ?x. Beth bynnag yw gwerth ?y, rhaid i ?x fod yn (b ?y). Felly rhoddir rhwymiad ?x i'r patrwm (b ?y) yn y ffrâm. Os pennir gwerth ar gyfer ?y yn ddiweddarach a'i ychwanegu at y ffrâm (drwy baru neu uno patrymau y mae'n rhaid iddo fod yn gyson â'r ffrâm hon), bydd yr ?x a rwymwyd yn flaenorol yn cyfeirio at y gwerth hwn.²⁷⁶

Cymhwyso rheolau

Uno patrymau yw'r allwedd i'r gydran o'r system ymholi sy'n gwneud casgliadau o reolau. I weld sut y cyflawnir hyn, ystyriwch brosesu ymholiad sy'n cynnwys cymhwyso rheol, megis

(lives-near ?x (Hacker Alyssa P))

I brosesu'r ymholiad hwn, defnyddiwn yn gyntaf y weithdrefn paru patrymau arferol a ddisgrifir uchod i weld a oes unrhyw haeriadau yn y gronfa ddata sy'n cyfateb i'r patrwm hwn. (Ni fydd rhai yn yr achos hwn, gan nad yw ein cronfa ddata'n cynnwys haeriadau uniongyrchol am bwy sy'n byw'n agos at bwy.) Y cam nesaf yw ceisio uno patrwm yr ymholiad â chasgliad pob rheol. Canfyddwn fod y patrwm yn uno â chasgliad y rheol

(rule (lives-near ?person-1 ?person-2)
      (and (address ?person-1 
                    (?town . ?rest-1))
           (address ?person-2 
                    (?town . ?rest-2))
           (not (same ?person-1 ?person-2))))

gan arwain at ffrâm sy'n pennu bod ?person-2 wedi'i rwymo i (Hacker Alyssa P) ac y dylai ?x gael ei rwymo i ?person-1 (cael yr un gwerth ag ef). Nawr, mewn perthynas â'r ffrâm hon, gwerthuswn yr ymholiad cyfansawdd a roddir gan gorff y rheol. Bydd cyfatebiadau llwyddiannus yn ymestyn y ffrâm hon drwy ddarparu rhwymiad ar gyfer ?person-1, ac o ganlyniad gwerth ar gyfer ?x, y gallwn ei ddefnyddio i enghreifftio patrwm gwreiddiol yr ymholiad.

Yn gyffredinol, mae'r gwerthusydd ymholi'n defnyddio'r dull canlynol i gymhwyso rheol wrth geisio sefydlu patrwm ymholiad mewn ffrâm sy'n pennu rhwymiadau ar gyfer rhai o newidynnau'r patrwm:

Uno'r ymholiad â chasgliad y rheol i ffurfio, os yw'n llwyddiannus, estyniad i'r ffrâm wreiddiol.
Mewn perthynas â'r ffrâm estynedig, gwerthuso'r ymholiad a ffurfir gan gorff y rheol.

Sylwch mor debyg yw hyn i'r dull o gymhwyso gweithdrefn yn y gwerthusydd eval/apply ar gyfer Lisp:

Rhwymo paramedrau'r weithdrefn i'w hargiau i ffurfio ffrâm sy'n ymestyn amgylchedd gwreiddiol y weithdrefn.
Mewn perthynas â'r amgylchedd estynedig, gwerthuso'r mynegiad a ffurfir gan gorff y weithdrefn.

Ni ddylai'r tebygrwydd rhwng y ddau werthusydd beri syndod. Yn union fel mai diffiniadau gweithdrefnau yw'r dull haniaethu yn Lisp, diffiniadau rheolau yw'r dull haniaethu yn yr iaith ymholi. Ym mhob achos, datodwn yr haniaeth drwy greu rhwymiadau priodol a gwerthuso corff y rheol neu'r weithdrefn mewn perthynas â'r rhain.

Ymholiadau syml

Gwelsom yn gynharach yn yr adran hon sut i werthuso ymholiadau syml heb reolau. Gan ein bod bellach wedi gweld sut i gymhwyso rheolau, gallwn ddisgrifio sut i werthuso ymholiadau syml gan ddefnyddio rheolau a haeriadau.

O gael patrwm yr ymholiad a ffrwd o fframiau, cynhyrchwn ddwy ffrwd ar gyfer pob ffrâm yn y ffrwd fewnbwn:

ffrwd o fframiau estynedig a geir drwy baru'r patrwm â phob haeriad yn y gronfa ddata (gan ddefnyddio'r parwr patrymau), a
ffrwd o fframiau estynedig a geir drwy gymhwyso pob rheol bosibl (gan ddefnyddio'r unydd).²⁷⁷

Mae atodi'r ddwy ffrwd hyn yn cynhyrchu ffrwd sy'n cynnwys yr holl ffyrdd y gellir bodloni'r patrwm a roddwyd yn gyson â'r ffrâm wreiddiol. Cyfunir yr holl ffrydiau hyn (un ar gyfer pob ffrâm yn y ffrwd fewnbwn) nawr i ffurfio un ffrwd fawr, sydd felly'n cynnwys yr holl ffyrdd y gellir ymestyn unrhyw un o'r fframiau yn y ffrwd fewnbwn wreiddiol i gynhyrchu cyfatebiad â'r patrwm a roddwyd.

Y gwerthusydd ymholi a'r ddolen yrru

Er gwaethaf cymhlethdod y gweithrediadau paru sylfaenol, mae'r system wedi'i threfnu'n debyg iawn i werthusydd ar gyfer unrhyw iaith. Gelwir y weithdrefn sy'n cydlynu'r gweithrediadau paru yn qeval, ac mae'n chwarae rôl sy'n cyfateb i rôl gweithdrefn eval Lisp. Mae Qeval yn cymryd ymholiad a ffrwd o fframiau fel mewnbynnau. Ei hallbwn yw ffrwd o fframiau, sy'n cyfateb i bariadau llwyddiannus â phatrwm yr ymholiad, sy'n ymestyn rhyw ffrâm yn y ffrwd fewnbwn, fel y dangosir yn Ffigur 4.4. Fel eval, mae qeval yn dosbarthu'r gwahanol fathau o fynegiadau (ymholiadau) ac yn dethol gweithdrefn briodol ar gyfer pob un. Mae gweithdrefn ar gyfer pob ffurf arbennig (and, or, not, ac lisp-value) ac un ar gyfer ymholiadau syml.

Mae'r ddolen yrru, sy'n cyfateb i'r weithdrefn driver-loop ar gyfer y gwerthusyddion eraill yn y bennod hon, yn darllen ymholiadau o'r derfynell. Ar gyfer pob ymholiad, mae'n galw qeval gyda'r ymholiad a ffrwd sy'n cynnwys un ffrâm wag. Bydd hyn yn cynhyrchu ffrwd pob cyfatebiad posibl (pob estyniad posibl i'r ffrâm wag). Ar gyfer pob ffrâm yn y ffrwd sy'n deillio o hynny, mae'n enghreifftio'r ymholiad gwreiddiol gan ddefnyddio gwerthoedd y newidynnau a geir yn y ffrâm. Yna argreffir y ffrwd hon o ymholiadau wedi'u henghreifftio.²⁷⁸

Mae'r gyrrwr hefyd yn gwirio am y gorchymyn arbennig assert!, sy'n arwyddo nad ymholiad yw'r mewnbwn ond yn hytrach haeriad neu reol i'w hychwanegu at y gronfa ddata. Er enghraifft,

(assert!
 (job (Bitdiddle Ben)
      (computer wizard)))

(assert!
 (rule (wheel ?person)
       (and (supervisor 
             ?middle-manager ?person)
            (supervisor
             ?x ?middle-manager))))

4.4.3Ai Rhesymeg Fathemategol yw Rhaglennu Rhesymegol?

Gall y dulliau cyfuno a ddefnyddir yn yr iaith ymholi ymddangos ar y dechrau yn union yr un fath â gweithrediadau and, or, ac not rhesymeg fathemategol, ac yn wir cyflawnir cymhwyso rheolau'r iaith ymholi drwy ddull casglu dilys.²⁷⁹ Fodd bynnag, nid yw'r uniaethu hwn rhwng yr iaith ymholi a rhesymeg fathemategol yn ddilys mewn gwirionedd, oherwydd mae'r iaith ymholi'n darparu strwythur rheoli sy'n dehongli'r datganiadau rhesymegol yn weithdrefnol. Gallwn yn aml fanteisio ar y strwythur rheoli hwn. Er enghraifft, i ganfod holl oruchwylwyr rhaglenwyr gallem lunio ymholiad mewn un o ddwy ffurf sy'n rhesymegol gyfwerth:

(and (job ?x (computer programmer))
     (supervisor ?x ?y))

neu

(and (supervisor ?x ?y)
     (job ?x (computer programmer)))

Os oes gan gwmni lawer mwy o oruchwylwyr na rhaglenwyr (yr achos arferol), mae'n well defnyddio'r ffurf gyntaf yn hytrach na'r ail, oherwydd mae'n rhaid sganio'r gronfa ddata ar gyfer pob canlyniad canolraddol (ffrâm) a gynhyrchir gan gymal cyntaf yr and.

Nod rhaglennu rhesymegol yw darparu technegau i'r rhaglennydd ar gyfer dadelfennu problem gyfrifiadurol yn ddwy broblem ar wahân: “beth” sydd i'w gyfrifo, a “sut” y dylid ei gyfrifo. Cyflawnir hyn drwy ddewis is-set o ddatganiadau rhesymeg fathemategol sy'n ddigon pwerus i allu disgrifio unrhyw beth y gallai rhywun ddymuno ei gyfrifo, ond eto'n ddigon gwan i gael dehongliad gweithdrefnol y gellir ei reoli. Y bwriad yma yw, ar y naill law, y dylai rhaglen a bennir mewn iaith raglennu resymegol fod yn rhaglen effeithiol y gall cyfrifiadur ei chyflawni. Cyflawnir rheolaeth (“sut” i gyfrifo) drwy ddefnyddio trefn gwerthuso'r iaith. Dylem allu trefnu trefn y cymalau a threfn yr is-nodau o fewn pob cymal fel y gwneir y cyfrifiad mewn trefn a ystyrir yn effeithiol ac yn effeithlon. Ar yr un pryd, dylem allu gweld canlyniad y cyfrifiad (“beth” i'w gyfrifo) fel canlyniad syml i ddeddfau rhesymeg.

Gellir ystyried ein hiaith ymholi'n union fel is-set o'r fath o resymeg fathemategol y gellir ei dehongli'n weithdrefnol. Mae haeriad yn cynrychioli ffaith syml (gosodiad atomig). Mae rheol yn cynrychioli'r goblygiad bod casgliad y rheol yn dal yn yr achosion hynny lle mae corff y rheol yn dal. Mae gan reol ddehongliad gweithdrefnol naturiol: I sefydlu casgliad y rheol, sefydlwch gorff y rheol. Mae rheolau, felly, yn pennu cyfrifiadau. Fodd bynnag, oherwydd y gellir ystyried rheolau hefyd yn ddatganiadau rhesymeg fathemategol, gallwn gyfiawnhau unrhyw “gasgliad” a gyflawnir gan raglen resymegol drwy haeru y gellid cael yr un canlyniad drwy weithio'n gyfan gwbl o fewn rhesymeg fathemategol.²⁸⁰

Dolenni anfeidraidd

Un o ganlyniadau dehongli rhaglenni rhesymegol yn weithdrefnol yw ei bod yn bosibl adeiladu rhaglenni aneffeithlon anobeithiol ar gyfer datrys problemau penodol. Mae achos eithafol o aneffeithlonrwydd yn digwydd pan fydd y system yn syrthio i ddolenni anfeidraidd wrth wneud diddwythiadau. Fel enghraifft syml, tybiwch ein bod yn sefydlu cronfa ddata o briodasau enwog, gan gynnwys

(assert! (married Minnie Mickey))

Os gofynnwn nawr

(married Mickey ?who)

ni chawn ymateb, gan nad yw'r system yn gwybod, os yw $A$ yn briod ag $B$ , fod $B$ yn briod ag $A$ . Felly haerwn y rheol

(assert! (rule (married ?x ?y)
               (married ?y ?x)))

ac ymholwn eto

(married Mickey ?who)

Yn anffodus, bydd hyn yn gyrru'r system i ddolen anfeidraidd, fel a ganlyn:

Mae'r system yn canfod bod y rheol married yn gymwys; hynny yw, mae casgliad y rheol (married ?x ?y) yn uno'n llwyddiannus â phatrwm yr ymholiad (married Mickey ?who) i gynhyrchu ffrâm lle mae ?x wedi'i rwymo i Mickey ac ?y wedi'i rwymo i ?who. Felly mae'r dehonglydd yn mynd ymlaen i werthuso corff y rheol (married ?y ?x) yn y ffrâm hon—i bob pwrpas, prosesu'r ymholiad (married ?who Mickey).
Mae un ateb yn ymddangos yn uniongyrchol fel haeriad yn y gronfa ddata: (married Minnie Mickey).
Mae'r rheol married hefyd yn gymwys, felly mae'r dehonglydd yn gwerthuso corff y rheol eto, sydd y tro hwn yn gyfwerth ag (married Mickey ?who).

Mae'r system bellach mewn dolen anfeidraidd. Yn wir, mae p'un a fydd y system yn canfod yr ateb syml (married Minnie Mickey) cyn mynd i'r ddolen yn dibynnu ar fanylion gweithredu ynghylch y drefn y mae'r system yn gwirio eitemau'r gronfa ddata ynddi. Mae hon yn enghraifft syml iawn o'r mathau o ddolenni a all ddigwydd. Gall casgliadau o reolau sy'n rhyngberthyn arwain at ddolenni sy'n llawer anoddach eu rhagweld, a gall ymddangosiad dolen ddibynnu ar drefn cymalau mewn and (gweler Ymarfer 4.64) neu ar fanylion lefel isel ynghylch y drefn y mae'r system yn prosesu ymholiadau ynddi.²⁸¹

Problemau gydag `not`

Mae hynodrwydd arall yn y system ymholi'n ymwneud ag not. O gael cronfa ddata 4.4.1, ystyriwch y ddau ymholiad canlynol:

(and (supervisor ?x ?y)
     (not (job ?x (computer programmer))))

(and (not (job ?x (computer programmer)))
     (supervisor ?x ?y))

Nid yw'r ddau ymholiad hyn yn cynhyrchu'r un canlyniad. Mae'r ymholiad cyntaf yn dechrau drwy ganfod pob cofnod yn y gronfa ddata sy'n cyfateb i (supervisor ?x ?y), ac yna'n hidlo'r fframiau sy'n deillio o hynny drwy dynnu'r rhai lle mae gwerth ?x yn bodloni (job ?x (computer programmer)). Mae'r ail ymholiad yn dechrau drwy hidlo'r fframiau sy'n dod i mewn i dynnu'r rhai a all fodloni (job ?x (computer programmer)). Gan mai'r unig ffrâm sy'n dod i mewn yw ffrâm wag, mae'n gwirio'r gronfa ddata i weld a oes unrhyw batrymau sy'n bodloni (job ?x (computer programmer)). Gan fod cofnodion o'r ffurf hon yn gyffredinol, mae'r cymal not yn hidlo'r ffrâm wag allan ac yn dychwelyd ffrwd wag o fframiau. O ganlyniad, mae'r ymholiad cyfansawdd cyfan yn dychwelyd ffrwd wag.

Y broblem yw bod ein gweithrediad o not wedi'i fwriadu mewn gwirionedd i wasanaethu fel hidlydd ar werthoedd y newidynnau. Os prosesir cymal not gyda ffrâm lle mae rhai o'r newidynnau'n aros heb eu rhwymo (fel y mae ?x yn yr enghraifft uchod), bydd y system yn cynhyrchu canlyniadau annisgwyl. Mae problemau tebyg yn digwydd wrth ddefnyddio lisp-value—ni all traethiad Lisp weithio os yw rhai o'i argiau heb eu rhwymo. Gweler Ymarfer 4.77.

Mae ffordd lawer mwy difrifol hefyd y mae not yr iaith ymholi'n wahanol i not rhesymeg fathemategol. Mewn rhesymeg, dehonglwn y datganiad “nid $P$ ” i olygu nad yw $P$ yn wir. Yn y system ymholi, fodd bynnag, mae “nid $P$ ” yn golygu na ellir diddwytho $P$ o'r wybodaeth yn y gronfa ddata. Er enghraifft, o gael cronfa ddata personél 4.4.1, byddai'r system yn ddigon hapus i ddiddwytho pob math o ddatganiadau not, megis nad yw Ben Bitdiddle yn gefnogwr pêl fas, nad yw'n bwrw glaw y tu allan, ac nad yw 2 + 2 yn 4.²⁸² Mewn geiriau eraill, mae not ieithoedd rhaglennu rhesymegol yn adlewyrchu'r hyn a elwir yn dybiaeth byd caeedig, sef bod yr holl wybodaeth berthnasol wedi'i chynnwys yn y gronfa ddata.²⁸³

Ymarfer 4.64: Mae Louis Reasoner yn dileu'r rheol outranked-by (4.4.1) o'r gronfa ddata ar gam. Pan mae'n sylweddoli hyn, mae'n ei hailosod yn gyflym. Yn anffodus, mae'n gwneud newid bach yn y rheol, ac yn ei theipio fel
(rule (outranked-by ?staff-person ?boss)
  (or (supervisor ?staff-person ?boss)
      (and (outranked-by ?middle-manager
                         ?boss)
           (supervisor ?staff-person 
                       ?middle-manager))))
Yn union ar ôl i Louis deipio'r wybodaeth hon i mewn i'r system, daw DeWitt Aull heibio i ganfod pwy sy'n uwch na Ben Bitdiddle yn yr hierarchaeth. Mae'n cyflwyno'r ymholiad
(outranked-by (Bitdiddle Ben) ?who)
Ar ôl ateb, mae'r system yn mynd i ddolen anfeidraidd. Eglurwch pam.

Ymarfer 4.65: Mae Cy D. Fect, sy'n edrych ymlaen at y diwrnod pan fydd yn codi yn y sefydliad, yn rhoi ymholiad i ganfod yr holl benaethiaid (gan ddefnyddio rheol wheel 4.4.1):
(wheel ?who)
Er ei syndod, mae'r system yn ymateb
;;; Query results:
(wheel (Warbucks Oliver))
(wheel (Bitdiddle Ben))
(wheel (Warbucks Oliver))
(wheel (Warbucks Oliver))
(wheel (Warbucks Oliver))
Pam mae Oliver Warbucks wedi'i restru bedair gwaith?

Ymarfer 4.66: Mae Ben wedi bod yn cyffredinoli'r system ymholi i ddarparu ystadegau am y cwmni. Er enghraifft, i ganfod cyfanswm cyflogau'r holl raglenwyr cyfrifiaduron bydd modd dweud
(sum ?amount
     (and (job ?x (computer programmer))
          (salary ?x ?amount)))
Yn gyffredinol, mae system newydd Ben yn caniatáu mynegiadau o'r ffurf
(accumulation-function ⟨variable⟩
                       ⟨query pattern⟩)
lle gall accumulation-function fod yn bethau fel sum, average, neu maximum. Mae Ben yn rhesymu y dylai gweithredu hyn fod yn hawdd iawn. Y cyfan a wna yw bwydo patrwm yr ymholiad i qeval. Bydd hyn yn cynhyrchu ffrwd o fframiau. Yna bydd yn pasio'r ffrwd hon drwy ffwythiant mapio sy'n tynnu gwerth y newidyn dynodedig o bob ffrâm yn y ffrwd ac yn bwydo'r ffrwd o werthoedd sy'n deillio o hynny i'r ffwythiant cronni. Yn union wrth i Ben gwblhau'r gweithrediad a pharatoi i roi cynnig arno, mae Cy yn cerdded heibio, yn dal i bendroni dros ganlyniad yr ymholiad wheel yn Ymarfer 4.65. Pan mae Cy yn dangos ymateb y system i Ben, mae Ben yn griddfan, “O, na, ni fydd fy nghynllun cronni syml yn gweithio!”

Beth mae Ben newydd ei sylweddoli? Amlinellwch ddull y gall ei ddefnyddio i achub y sefyllfa.

Ymarfer 4.67: Dyfeisiwch ffordd o osod canfodydd dolenni yn y system ymholi er mwyn osgoi'r mathau o ddolenni syml a ddangosir yn y testun ac yn Ymarfer 4.64. Y syniad cyffredinol yw y dylai'r system gadw rhyw fath o hanes o'i chadwyn bresennol o ddiddwythiadau ac na ddylai ddechrau prosesu ymholiad y mae eisoes yn gweithio arno. Disgrifiwch pa fath o wybodaeth (patrymau a fframiau) a gynhwysir yn yr hanes hwn, a sut y dylid gwneud y gwiriad. (Ar ôl ichi astudio manylion gweithrediad y system ymholi yn 4.4.4, efallai y byddwch am addasu'r system i gynnwys eich canfodydd dolenni.)

Ymarfer 4.68: Diffiniwch reolau i weithredu gweithrediad reverse Ymarfer 2.18, sy'n dychwelyd rhestr sy'n cynnwys yr un elfennau â rhestr a roddwyd, yn y drefn wrthdro. (Awgrym: Defnyddiwch append-to-form.) A all eich rheolau ateb (reverse (1 2 3) ?x) ac (reverse ?x (1 2 3)) ill dau?

Ymarfer 4.69: Gan ddechrau â'r gronfa ddata a'r rheolau a luniwyd gennych yn Ymarfer 4.63, dyfeisiwch reol ar gyfer ychwanegu “gor-” at berthynas ŵyr. Dylai hyn alluogi'r system i ddiddwytho bod Irad yn orŵyr i Adam, neu fod Jabal a Jubal yn ddisgynyddion gwrywaidd i Adam saith cenhedlaeth yn ddiweddarach. (Awgrym: Cynrychiolwch y ffaith am Irad, er enghraifft, fel ((great grandson) Adam Irad). Ysgrifennwch reolau sy'n pennu a yw rhestr yn gorffen â'r gair grandson. Defnyddiwch hyn i fynegi rheol sy'n caniatáu deillio'r berthynas ((great . ?rel) ?x ?y), lle mae ?rel yn rhestr sy'n gorffen ag grandson.) Gwiriwch eich rheolau ar ymholiadau megis ((great grandson) ?g ?ggs) ac (?relationship Adam Irad).

4.4.4Gweithredu'r System Ymholi

Disgrifiodd Adran 4.4.2 sut mae'r system ymholi'n gweithio. Nawr llenwn y manylion drwy gyflwyno gweithrediad cyflawn o'r system.

4.4.4.1Y Ddolen Yrru ac Enghreifftio

Mae dolen yrru'r system ymholi yn darllen mynegiadau mewnbwn dro ar ôl tro. Os yw'r mynegiad yn rheol neu'n haeriad i'w ychwanegu at y gronfa ddata, yna ychwanegir y wybodaeth. Fel arall, tybir bod y mynegiad yn ymholiad. Mae'r gyrrwr yn pasio'r ymholiad hwn i'r gwerthusydd qeval ynghyd â ffrwd fframiau gychwynnol sy'n cynnwys un ffrâm wag. Canlyniad y gwerthuso yw ffrwd o fframiau a gynhyrchir drwy fodloni'r ymholiad â gwerthoedd newidynnau a geir yn y gronfa ddata. Defnyddir y fframiau hyn i ffurfio ffrwd newydd sy'n cynnwys copïau o'r ymholiad gwreiddiol lle enghreifftir y newidynnau â gwerthoedd a ddarperir gan y ffrwd fframiau, ac argraffir y ffrwd derfynol hon yn y derfynell:

(define input-prompt  ";;; Query input:")
(define output-prompt ";;; Query results:")

(define (query-driver-loop)
  (prompt-for-input input-prompt)
  (let ((q (query-syntax-process (read))))
    (cond ((assertion-to-be-added? q)
           (add-rule-or-assertion! 
            (add-assertion-body q))
           (newline)
           (display 
            "Assertion added to data base.")
           (query-driver-loop))
          (else
           (newline)
           (display output-prompt)
           (display-stream
            (stream-map
             (lambda (frame)
               (instantiate
                q
                frame
                (lambda (v f)
                  (contract-question-mark v))))
             (qeval q (singleton-stream '()))))
           (query-driver-loop)))))

Yma, fel yn y gwerthusyddion eraill yn y bennod hon, defnyddiwn gystrawen haniaethol ar gyfer mynegiadau'r iaith ymholi. Rhoddir gweithrediad cystrawen y mynegiadau, gan gynnwys y traethiad assertion-to-be-added? a'r detholwr add-assertion-body, yn 4.4.4.7. Diffinnir Add-rule-or-assertion! yn 4.4.4.5.

Cyn gwneud unrhyw brosesu ar fynegiad mewnbwn, mae'r ddolen yrru yn ei drawsffurfio'n gystrawennol i ffurf sy'n gwneud y prosesu'n fwy effeithlon. Mae hyn yn cynnwys newid cynrychioliad newidynnau patrwm. Pan enghreifftir yr ymholiad, trosir unrhyw newidynnau sydd heb eu rhwymo yn ôl i'r cynrychioliad mewnbwn cyn eu hargraffu. Cyflawnir y trawsffurfiadau hyn gan y ddwy weithdrefn query-syntax-process ac contract-question-mark (4.4.4.7).

I enghreifftio mynegiad, copïwn ef, gan roi gwerthoedd unrhyw newidynnau yn y mynegiad mewn ffrâm benodol yn eu lle. Enghreifftir y gwerthoedd eu hunain, gan y gallent gynnwys newidynnau (er enghraifft, os yw ?x yn exp wedi'i rwymo i ?y o ganlyniad i uno ac os yw ?y yn ei dro wedi'i rwymo i 5). Rhoddir y weithred i'w chyflawni os na ellir enghreifftio newidyn gan arg gweithdrefnol i instantiate.

(define (instantiate 
         exp frame unbound-var-handler)
  (define (copy exp)
    (cond ((var? exp)
           (let ((binding 
                  (binding-in-frame 
                   exp frame)))
             (if binding
                 (copy 
                  (binding-value binding))
                 (unbound-var-handler 
                  exp frame))))
          ((pair? exp)
           (cons (copy (car exp)) 
                 (copy (cdr exp))))
          (else exp)))
  (copy exp))

Diffinnir y gweithdrefnau sy'n trin rhwymiadau yn 4.4.4.8.

4.4.4.2Y Gwerthusydd

Y weithdrefn qeval, a elwir gan yr query-driver-loop, yw gwerthusydd sylfaenol y system ymholi. Mae'n cymryd ymholiad a ffrwd o fframiau yn fewnbynnau, ac yn dychwelyd ffrwd o fframiau wedi'u hymestyn. Mae'n adnabod ffurfiau arbennig drwy ddethol gweithdrefn a gyfarwyddir gan ddata gan ddefnyddio get ac put, yn union fel y gwnaethom wrth weithredu gweithrediadau generig ym Mhennod 2. Tybir bod unrhyw ymholiad nad yw'n cael ei adnabod yn ffurf arbennig yn ymholiad syml, i'w brosesu gan simple-query.

(define (qeval query frame-stream)
  (let ((qproc (get (type query) 'qeval)))
    (if qproc
        (qproc (contents query) frame-stream)
        (simple-query query frame-stream))))

Mae Type ac contents, a ddiffinnir yn 4.4.4.7, yn gweithredu cystrawen haniaethol y ffurfiau arbennig.

Ymholiadau syml

Mae'r weithdrefn simple-query yn trin ymholiadau syml. Mae'n cymryd ymholiad syml (patrwm) ynghyd â ffrwd o fframiau yn argiau, ac yn dychwelyd y ffrwd a ffurfir drwy ymestyn pob ffrâm â holl gyfatebiaethau'r ymholiad yn y gronfa ddata.

(define (simple-query query-pattern 
                      frame-stream)
  (stream-flatmap
   (lambda (frame)
     (stream-append-delayed
      (find-assertions query-pattern frame)
      (delay 
        (apply-rules query-pattern frame))))
   frame-stream))

Ar gyfer pob ffrâm yn y ffrwd fewnbwn, defnyddiwn find-assertions (4.4.4.3) i baru'r patrwm yn erbyn yr holl haeriadau yn y gronfa ddata, gan gynhyrchu ffrwd o fframiau wedi'u hymestyn, a defnyddiwn apply-rules (4.4.4.4) i gymhwyso'r holl reolau posibl, gan gynhyrchu ffrwd arall o fframiau wedi'u hymestyn. Cyfunir y ddwy ffrwd hyn (gan ddefnyddio stream-append-delayed, 4.4.4.6) i wneud ffrwd o'r holl ffyrdd y gellir bodloni'r patrwm a roddwyd yn gyson â'r ffrâm wreiddiol (gweler Ymarfer 4.71). Cyfunir ffrydiau'r fframiau mewnbwn unigol gan ddefnyddio stream-flatmap (4.4.4.6) i ffurfio un ffrwd fawr o'r holl ffyrdd y gellir ymestyn unrhyw un o'r fframiau yn y ffrwd fewnbwn wreiddiol i gynhyrchu cyfatebiaeth â'r patrwm a roddwyd.

Ymholiadau cyfansawdd

Trinnir ymholiadau And fel y dangosir yn Ffigur 4.5 gan y weithdrefn conjoin. Mae Conjoin yn cymryd y cydgymalau a'r ffrwd fframiau yn fewnbynnau ac yn dychwelyd y ffrwd o fframiau wedi'u hymestyn. Yn gyntaf, mae conjoin yn prosesu'r ffrwd o fframiau i ganfod ffrwd yr holl estyniadau ffrâm posibl sy'n bodloni'r ymholiad cyntaf yn y cydgysylltiad. Yna, gan ddefnyddio hon yn ffrwd fframiau newydd, mae'n cymhwyso conjoin yn ddychweliadol i weddill yr ymholiadau.

(define (conjoin conjuncts frame-stream)
  (if (empty-conjunction? conjuncts)
      frame-stream
      (conjoin (rest-conjuncts conjuncts)
               (qeval 
                (first-conjunct conjuncts)
                frame-stream))))

Mae'r mynegiad

(put 'and 'qeval conjoin)

yn gosod qeval i ddethol conjoin pan geir ffurf and.

Trinnir ymholiadau Or yn yr un modd, fel y dangosir yn Ffigur 4.6. Cyfrifir ffrydiau allbwn amrywiol ddatgymalau'r or ar wahân a'u cyfuno gan ddefnyddio'r weithdrefn interleave-delayed o 4.4.4.6. (Gweler Ymarfer 4.71 ac Ymarfer 4.72.)

(define (disjoin disjuncts frame-stream)
  (if (empty-disjunction? disjuncts)
      the-empty-stream
      (interleave-delayed
       (qeval (first-disjunct disjuncts) 
              frame-stream)
       (delay (disjoin 
               (rest-disjuncts disjuncts)
               frame-stream)))))
(put 'or 'qeval disjoin)

Rhoddir y traethiadau a'r detholwyr ar gyfer cystrawen cydgymalau a datgymalau yn 4.4.4.7.

Hidlyddion

Trinnir Not gan y dull a amlinellir yn 4.4.2. Ceisiwn ymestyn pob ffrâm yn y ffrwd fewnbwn i fodloni'r ymholiad sy'n cael ei negyddu, a chynhwyswn ffrâm benodol yn y ffrwd allbwn dim ond os na ellir ei hymestyn.

(define (negate operands frame-stream)
  (stream-flatmap
   (lambda (frame)
     (if (stream-null? 
          (qeval (negated-query operands)
                 (singleton-stream frame)))
         (singleton-stream frame)
         the-empty-stream))
   frame-stream))
(put 'not 'qeval negate)

Hidlydd tebyg i not yw Lisp-value. Defnyddir pob ffrâm yn y ffrwd i enghreifftio'r newidynnau yn y patrwm, cymhwysir y traethiad a nodir, a hidlir y fframiau y mae'r traethiad yn dychwelyd anwir ar eu cyfer allan o'r ffrwd fewnbwn. Ceir gwall os oes newidynnau patrwm heb eu rhwymo.

(define (lisp-value call frame-stream)
  (stream-flatmap
   (lambda (frame)
     (if (execute
          (instantiate
           call
           frame
           (lambda (v f)
             (error 
              "Unknown pat var: LISP-VALUE" 
              v))))
         (singleton-stream frame)
         the-empty-stream))
   frame-stream))
(put 'lisp-value 'qeval lisp-value)

Rhaid i Execute, sy'n cymhwyso'r traethiad i'r argiau, ddefnyddio eval i werthuso mynegiad y traethiad er mwyn cael y weithdrefn i'w chymhwyso. Fodd bynnag, rhaid iddo beidio â gwerthuso'r argiau, gan mai'r argiau gwirioneddol ydynt eisoes, ac nid mynegiadau y bydd eu gwerthuso (yn Lisp) yn cynhyrchu'r argiau. Sylwch y gweithredir execute gan ddefnyddio eval ac apply o'r system Lisp sylfaenol.

(define (execute exp)
  (apply (eval (predicate exp) 
               user-initial-environment)
         (args exp)))

Mae'r ffurf arbennig always-true yn darparu ar gyfer ymholiad a fodlonir bob amser. Mae'n anwybyddu ei gynnwys (sy'n wag fel arfer) ac yn pasio'r holl fframiau yn y ffrwd fewnbwn drwyddo yn unig. Defnyddir Always-true gan y detholwr rule-body (4.4.4.7) i ddarparu cyrff i reolau a ddiffiniwyd heb gyrff (hynny yw, rheolau y bodlonir eu casgliadau bob amser).

(define (always-true ignore frame-stream) 
  frame-stream)
(put 'always-true 'qeval always-true)

Rhoddir y detholwyr sy'n diffinio cystrawen not ac lisp-value yn 4.4.4.7.

4.4.4.3Canfod Haeriadau drwy Baru Patrymau

Mae Find-assertions, a elwir gan simple-query (4.4.4.2), yn cymryd patrwm a ffrâm yn fewnbwn. Mae'n dychwelyd ffrwd o fframiau, pob un yn ymestyn yr un a roddwyd drwy gyfatebiaeth yn y gronfa ddata â'r patrwm a roddwyd. Mae'n defnyddio fetch-assertions (4.4.4.5) i gael ffrwd o'r holl haeriadau yn y gronfa ddata y dylid eu gwirio am gyfatebiaeth â'r patrwm a'r ffrâm. Y rheswm dros fetch-assertions yma yw y gallwn yn aml gymhwyso profion syml a fydd yn dileu llawer o gofnodion y gronfa ddata o'r grŵp o ymgeiswyr am gyfatebiaeth lwyddiannus. Byddai'r system yn dal i weithio pe baem yn dileu fetch-assertions ac yn gwirio ffrwd o'r holl haeriadau yn y gronfa ddata yn unig, ond byddai'r cyfrifiad yn llai effeithlon am y byddai angen inni wneud llawer mwy o alwadau i'r parwr.

(define (find-assertions pattern frame)
  (stream-flatmap 
    (lambda (datum) 
      (check-an-assertion datum pattern frame))
    (fetch-assertions pattern frame)))

Mae Check-an-assertion yn cymryd patrwm, gwrthrych data (haeriad), a ffrâm yn argiau, ac yn dychwelyd naill ai ffrwd un elfen sy'n cynnwys y ffrâm wedi'i hymestyn neu the-empty-stream os yw'r paru'n methu.

(define (check-an-assertion 
         assertion query-pat query-frame)
  (let ((match-result
         (pattern-match 
          query-pat assertion query-frame)))
    (if (eq? match-result 'failed)
        the-empty-stream
        (singleton-stream match-result))))

Mae'r parwr patrymau sylfaenol yn dychwelyd naill ai'r symbol failed neu estyniad o'r ffrâm a roddwyd. Syniad sylfaenol y parwr yw gwirio'r patrwm yn erbyn y data, elfen wrth elfen, gan gronni rhwymiadau ar gyfer newidynnau'r patrwm. Os yw'r patrwm a'r gwrthrych data yr un fath, mae'r paru'n llwyddo a dychwelwn y ffrâm o rwymiadau a gronnwyd hyd hynny. Fel arall, os yw'r patrwm yn newidyn, estynnwn y ffrâm bresennol drwy rwymo'r newidyn i'r data, cyn belled â bod hyn yn gyson â'r rhwymiadau sydd eisoes yn y ffrâm. Os yw'r patrwm a'r data ill dau'n barau, parwn (yn ddychweliadol) car y patrwm yn erbyn car y data i gynhyrchu ffrâm; yn y ffrâm hon yna parwn cdr y patrwm yn erbyn cdr y data. Os nad yw unrhyw un o'r achosion hyn yn berthnasol, mae'r paru'n methu a dychwelwn y symbol failed.

(define (pattern-match pat dat frame)
  (cond ((eq? frame 'failed) 'failed)
        ((equal? pat dat) frame)
        ((var? pat) 
         (extend-if-consistent 
          pat dat frame))
        ((and (pair? pat) (pair? dat))
         (pattern-match 
          (cdr pat) 
          (cdr dat)
          (pattern-match
           (car pat) (car dat) frame)))
        (else 'failed)))

Dyma'r weithdrefn sy'n ymestyn ffrâm drwy ychwanegu rhwymiad newydd, os yw hyn yn gyson â'r rhwymiadau sydd eisoes yn y ffrâm:

(define (extend-if-consistent var dat frame)
  (let ((binding (binding-in-frame var frame)))
    (if binding
        (pattern-match 
         (binding-value binding) dat frame)
        (extend var dat frame))))

Os nad oes rhwymiad i'r newidyn yn y ffrâm, ychwanegwn rwymiad y newidyn i'r data yn unig. Fel arall, parwn, yn y ffrâm, y data yn erbyn gwerth y newidyn yn y ffrâm. Os yw'r gwerth a storiwyd yn cynnwys cysonion yn unig, fel y mae'n rhaid os cafodd ei storio wrth baru patrymau gan extend-if-consistent, yna mae'r paru yn profi'n syml a yw'r gwerth a storiwyd a'r gwerth newydd yr un fath. Os ydynt, dychwelir y ffrâm heb ei haddasu; os nad ydynt, dychwelir arwydd methiant. Fodd bynnag, gall y gwerth a storiwyd gynnwys newidynnau patrwm os cafodd ei storio wrth uno (gweler 4.4.4.4). Bydd paru'r patrwm a storiwyd yn ddychweliadol yn erbyn y data newydd yn ychwanegu neu'n gwirio rhwymiadau i'r newidynnau yn y patrwm hwn. Er enghraifft, tybiwch fod gennym ffrâm lle mae ?x wedi'i rwymo i (f ?y) ac mae ?y heb ei rwymo, ac y dymunwn ychwanegu rhwymiad o ?x i (f b) at y ffrâm hon. Edrychwn am ?x a chanfod ei fod wedi'i rwymo i (f ?y). Mae hyn yn ein harwain i baru (f ?y) yn erbyn y gwerth newydd arfaethedig (f b) yn yr un ffrâm. Yn y pen draw mae'r paru hwn yn ymestyn y ffrâm drwy ychwanegu rhwymiad o ?y i b. Mae ?X yn aros wedi'i rwymo i (f ?y). Nid ydym byth yn addasu rhwymiad a storiwyd ac nid ydym byth yn storio mwy nag un rhwymiad i newidyn penodol.

Diffinnir y gweithdrefnau a ddefnyddir gan extend-if-consistent i drin rhwymiadau yn 4.4.4.8.

Patrymau â chynffonnau dotiog

Os yw patrwm yn cynnwys dot ac yna newidyn patrwm, mae'r newidyn patrwm yn paru â gweddill y rhestr ddata (yn hytrach nag elfen nesaf y rhestr ddata), yn union fel y disgwylid gyda'r nodiant cynffon ddotiog a ddisgrifir yn Ymarfer 2.20. Er nad yw'r parwr patrymau rydym newydd ei weithredu'n chwilio am ddotiau, mae'n ymddwyn fel y dymunwn. Y rheswm yw bod gweithrediad cyntefig Lisp read, a ddefnyddir gan query-driver-loop i ddarllen yr ymholiad a'i gynrychioli'n strwythur rhestrau, yn trin dotiau mewn ffordd arbennig.

Pan fydd read yn gweld dot, yn lle gwneud yr eitem nesaf yn elfen nesaf rhestr (sef car cons y bydd ei cdr yn weddill y rhestr), mae'n gwneud yr eitem nesaf yn cdr y strwythur rhestrau. Er enghraifft, gellid adeiladu'r strwythur rhestrau a gynhyrchir gan read ar gyfer y patrwm (computer ?type) drwy werthuso'r mynegiad (cons 'computer (cons '?type '())), a gellid adeiladu'r un ar gyfer (computer . ?type) drwy werthuso'r mynegiad (cons 'computer '?type).

Felly, wrth i pattern-match gymharu rhannau car ac cdr rhestr ddata a phatrwm a oedd â dot yn ddychweliadol, yn y pen draw mae'n paru'r newidyn ar ôl y dot (sef cdr y patrwm) yn erbyn is-restr o'r rhestr ddata, gan rwymo'r newidyn i'r rhestr honno. Er enghraifft, bydd paru'r patrwm (computer . ?type) yn erbyn (computer programmer trainee) yn paru ?type yn erbyn y rhestr (programmer trainee).

4.4.4.4Rheolau ac Uno

Apply-rules yw'r fersiwn rheolau o find-assertions (4.4.4.3). Mae'n cymryd patrwm a ffrâm yn fewnbwn, ac yn ffurfio ffrwd o fframiau estyniad drwy gymhwyso rheolau o'r gronfa ddata. Mae Stream-flatmap yn mapio apply-a-rule ar hyd y ffrwd o reolau a allai fod yn gymwys (a ddetholir gan fetch-rules, 4.4.4.5) ac yn cyfuno'r ffrydiau o fframiau a geir.

(define (apply-rules pattern frame)
  (stream-flatmap 
   (lambda (rule)
     (apply-a-rule rule pattern frame))
   (fetch-rules pattern frame)))

Mae Apply-a-rule yn cymhwyso rheolau gan ddefnyddio'r dull a amlinellir yn 4.4.2. Yn gyntaf mae'n ychwanegu at ei ffrâm arg drwy uno casgliad y rheol â'r patrwm yn y ffrâm a roddwyd. Os yw hyn yn llwyddo, mae'n gwerthuso corff y rheol yn y ffrâm newydd hon.

Cyn i ddim o hyn ddigwydd, fodd bynnag, mae'r rhaglen yn ailenwi'r holl newidynnau yn y rheol ag enwau newydd unigryw. Y rheswm yw atal drysu rhwng newidynnau ar gyfer gwahanol gymwysiadau o reolau. Er enghraifft, os yw dwy reol ill dwy'n defnyddio newidyn o'r enw ?x, yna gall pob un ychwanegu rhwymiad i ?x at y ffrâm pan gymhwysir hi. Nid oes gan y ddau ?x hyn ddim i'w wneud â'i gilydd, ac ni ddylem gael ein twyllo i feddwl bod rhaid i'r ddau rwymiad fod yn gyson. Yn hytrach nag ailenwi newidynnau, gallem ddyfeisio strwythur amgylchedd clyfrach; fodd bynnag, y dull ailenwi a ddewiswyd gennym yma yw'r un mwyaf uniongyrchol, hyd yn oed os nad y mwyaf effeithlon. (Gweler Ymarfer 4.79.) Dyma'r weithdrefn apply-a-rule:

(define (apply-a-rule rule
                      query-pattern
                      query-frame)
  (let ((clean-rule 
         (rename-variables-in rule)))
    (let ((unify-result
           (unify-match query-pattern
                        (conclusion clean-rule)
                        query-frame)))
      (if (eq? unify-result 'failed)
          the-empty-stream
          (qeval (rule-body clean-rule)
                 (singleton-stream 
                  unify-result))))))

Diffinnir y detholwyr rule-body ac conclusion sy'n tynnu rhannau rheol yn 4.4.4.7.

Cynhyrchwn enwau newidynnau unigryw drwy gysylltu dynodwr unigryw (megis rhif) â phob cymhwysiad o reol a chyfuno'r dynodwr hwn ag enwau gwreiddiol y newidynnau. Er enghraifft, os mai 7 yw dynodwr cymhwyso'r rheol, gallem newid pob ?x yn y rheol i ?x-7 a phob ?y yn y rheol i ?y-7. (Cynhwysir Make-new-variable ac new-rule-application-id gyda'r gweithdrefnau cystrawen yn 4.4.4.7.)

(define (rename-variables-in rule)
  (let ((rule-application-id 
         (new-rule-application-id)))
    (define (tree-walk exp)
      (cond ((var? exp)
             (make-new-variable 
              exp 
              rule-application-id))
            ((pair? exp)
             (cons (tree-walk (car exp))
                   (tree-walk (cdr exp))))
            (else exp)))
    (tree-walk rule)))

Gweithredir yr algorithm uno fel gweithdrefn sy'n cymryd dau batrwm a ffrâm yn fewnbynnau ac yn dychwelyd naill ai'r ffrâm wedi'i hymestyn neu'r symbol failed. Mae'r unwr yn debyg i'r parwr patrymau ac eithrio ei fod yn gymesur—caniateir newidynnau ar ddwy ochr y paru. Yn ei hanfod, mae Unify-match yr un fath ag pattern-match, ac eithrio bod cod ychwanegol (wedi'i nodi ag “***” isod) i drin yr achos lle mae'r gwrthrych ar ochr dde'r paru yn newidyn.

(define (unify-match p1 p2 frame)
  (cond ((eq? frame 'failed) 'failed)
        ((equal? p1 p2) frame)
        ((var? p1)
         (extend-if-possible p1 p2 frame))
        ((var? p2)
         (extend-if-possible 
          p2 
          p1 
          frame))        ; ***
        ((and (pair? p1) 
              (pair? p2))
         (unify-match 
          (cdr p1) 
          (cdr p2)
          (unify-match 
           (car p1)
           (car p2)
           frame)))
        (else 'failed)))

Wrth uno, fel wrth baru patrymau ar un ochr, dymunwn dderbyn estyniad arfaethedig o'r ffrâm dim ond os yw'n gyson â'r rhwymiadau presennol. Mae'r weithdrefn extend-if-possible a ddefnyddir wrth uno yr un fath â'r extend-if-consistent a ddefnyddir wrth baru patrymau, ac eithrio dau wiriad arbennig, wedi'u nodi ag “***” yn y rhaglen isod. Yn yr achos cyntaf, os yw'r newidyn rydym yn ceisio ei baru heb ei rwymo, ond bod y gwerth rydym yn ceisio ei baru ag ef ei hun yn newidyn (gwahanol), mae angen gwirio a yw'r gwerth wedi'i rwymo, ac os felly, paru ei werth. Os yw dwy ochr y paru heb eu rhwymo, gallwn rwymo'r naill i'r llall.

Mae'r ail wiriad yn ymdrin ag ymdrechion i rwymo newidyn i batrwm sy'n cynnwys y newidyn hwnnw. Gall sefyllfa o'r fath godi pryd bynnag yr ailadroddir newidyn yn y ddau batrwm. Ystyriwch, er enghraifft, uno'r ddau batrwm (?x ?x) ac (?y ⟨expression involving ?y⟩) mewn ffrâm lle mae ?x ac ?y ill dau heb eu rhwymo. Yn gyntaf parir ?x yn erbyn ?y, gan wneud rhwymiad o ?x i ?y. Nesaf, parir yr un ?x yn erbyn y mynegiad a roddwyd sy'n cynnwys ?y. Gan fod ?x eisoes wedi'i rwymo i ?y, mae hyn yn arwain at baru ?y yn erbyn y mynegiad. Os meddyliwn am yr unwr fel un sy'n canfod set o werthoedd ar gyfer newidynnau'r patrwm sy'n gwneud y patrymau'r un fath, yna mae'r patrymau hyn yn awgrymu cyfarwyddiadau i ganfod ?y fel bod ?y yn hafal i'r mynegiad sy'n cynnwys ?y. Nid oes dull cyffredinol o ddatrys hafaliadau o'r fath, felly gwrthodwn rwymiadau o'r fath; adnabyddir yr achosion hyn gan y traethiad depends-on?.²⁸⁴ Ar y llaw arall, nid ydym am wrthod ymdrechion i rwymo newidyn iddo'i hun. Er enghraifft, ystyriwch uno (?x ?x) ac (?y ?y). Mae'r ail ymgais i rwymo ?x i ?y yn paru ?y (gwerth ?x a storiwyd) yn erbyn ?y (gwerth newydd ?x). Ymdrinnir â hyn gan gymal equal? unify-match.

(define (extend-if-possible var val frame)
  (let ((binding (binding-in-frame var frame)))
    (cond (binding
           (unify-match
            (binding-value binding) val frame))
          ((var? val)                   ; ***
           (let ((binding 
                  (binding-in-frame 
                   val
                   frame)))
             (if binding
                 (unify-match
                  var 
                  (binding-value binding) 
                  frame)
                 (extend var val frame))))
          ((depends-on? val var frame)  ; ***
           'failed)
          (else (extend var val frame)))))

Traethiad yw Depends-on? sy'n profi a yw mynegiad a gynigir yn werth i newidyn patrwm yn dibynnu ar y newidyn. Rhaid gwneud hyn mewn perthynas â'r ffrâm bresennol am y gall y mynegiad gynnwys ymddangosiadau o newidyn sydd eisoes â gwerth sy'n dibynnu ar ein newidyn prawf. Mae strwythur depends-on? yn dramwyiad coeden dychweliadol syml lle rhown werthoedd newidynnau yn eu lle pryd bynnag y bo angen.

(define (depends-on? exp var frame)
  (define (tree-walk e)
    (cond ((var? e)
           (if (equal? var e)
               true
               (let
                 ((b (binding-in-frame 
                      e 
                      frame)))
                  (if b
                      (tree-walk 
                       (binding-value b))
                      false))))
          ((pair? e)
           (or (tree-walk (car e))
               (tree-walk (cdr e))))
          (else false)))
  (tree-walk exp))

4.4.4.5Cynnal y Gronfa Ddata

Un broblem bwysig wrth ddylunio ieithoedd rhaglennu rhesymegol yw trefnu pethau fel yr archwilir cyn lleied â phosibl o gofnodion amherthnasol y gronfa ddata wrth wirio patrwm penodol. Yn ein system, yn ogystal â storio'r holl haeriadau mewn un ffrwd fawr, storiwn yr holl haeriadau y mae eu car yn symbolau cyson mewn ffrydiau ar wahân, mewn tabl wedi'i fynegeio gan y symbol. I nôl haeriad a allai baru â phatrwm, gwiriwn yn gyntaf a yw car y patrwm yn symbol cyson. Os ydyw, dychwelwn (i'w profi gan ddefnyddio'r parwr) yr holl haeriadau a storiwyd sydd â'r un car. Os nad yw car y patrwm yn symbol cyson, dychwelwn yr holl haeriadau a storiwyd. Gallai dulliau clyfrach hefyd fanteisio ar wybodaeth yn y ffrâm, neu geisio optimeiddio'r achos lle nad yw car y patrwm yn symbol cyson hefyd. Osgown adeiladu ein meini prawf mynegeio (defnyddio'r car, a thrin achos symbolau cyson yn unig) yn uniongyrchol i'r rhaglen; yn lle hynny galwn ar draethiadau a detholwyr sy'n ymgorffori ein meini prawf.

(define THE-ASSERTIONS the-empty-stream)

(define (fetch-assertions pattern frame)
  (if (use-index? pattern)
      (get-indexed-assertions pattern)
      (get-all-assertions)))

(define (get-all-assertions) THE-ASSERTIONS)

(define (get-indexed-assertions pattern)
  (get-stream (index-key-of pattern)
              'assertion-stream))

Mae Get-stream yn chwilio am ffrwd yn y tabl ac yn dychwelyd ffrwd wag os nad oes dim wedi'i storio yno.

(define (get-stream key1 key2)
  (let ((s (get key1 key2)))
    (if s s the-empty-stream)))

Storir rheolau mewn ffordd debyg, gan ddefnyddio car casgliad y rheol. Fodd bynnag, patrymau mympwyol yw casgliadau rheolau, felly maent yn wahanol i haeriadau yn yr ystyr y gallant gynnwys newidynnau. Gall patrwm y mae ei car yn symbol cyson baru â rheolau y mae eu casgliadau'n dechrau â newidyn, yn ogystal â rheolau y mae gan eu casgliadau'r un car. Felly, wrth nôl rheolau a allai baru â phatrwm y mae ei car yn symbol cyson, nôlwn yr holl reolau y mae eu casgliadau'n dechrau â newidyn yn ogystal â'r rhai y mae gan eu casgliadau'r un car â'r patrwm. At y diben hwn storiwn yr holl reolau y mae eu casgliadau'n dechrau â newidyn mewn ffrwd ar wahân yn ein tabl, wedi'i mynegeio gan y symbol ?.

(define THE-RULES the-empty-stream)

(define (fetch-rules pattern frame)
  (if (use-index? pattern)
      (get-indexed-rules pattern)
      (get-all-rules)))

(define (get-all-rules) THE-RULES)

(define (get-indexed-rules pattern)
  (stream-append
   (get-stream (index-key-of pattern)
               'rule-stream)
   (get-stream '? 'rule-stream)))

Defnyddir Add-rule-or-assertion! gan query-driver-loop i ychwanegu haeriadau a rheolau at y gronfa ddata. Storir pob eitem yn y mynegai, os yw hynny'n briodol, ac mewn ffrwd o'r holl haeriadau neu reolau yn y gronfa ddata.

(define (add-rule-or-assertion! assertion)
  (if (rule? assertion)
      (add-rule! assertion)
      (add-assertion! assertion)))

(define (add-assertion! assertion)
  (store-assertion-in-index assertion)
  (let ((old-assertions THE-ASSERTIONS))
    (set! THE-ASSERTIONS
          (cons-stream assertion 
                       old-assertions))
    'ok))

(define (add-rule! rule)
  (store-rule-in-index rule)
  (let ((old-rules THE-RULES))
    (set! THE-RULES
          (cons-stream rule old-rules))
    'ok))

I storio haeriad neu reol mewn gwirionedd, gwiriwn a ellir ei fynegeio. Os gellir, storiwn ef yn y ffrwd briodol.

(define (store-assertion-in-index assertion)
  (if (indexable? assertion)
      (let ((key (index-key-of assertion)))
        (let ((current-assertion-stream
               (get-stream 
                key 'assertion-stream)))
          (put key
               'assertion-stream
               (cons-stream 
                assertion
                current-assertion-stream))))))

(define (store-rule-in-index rule)
  (let ((pattern (conclusion rule)))
    (if (indexable? pattern)
        (let ((key (index-key-of pattern)))
          (let ((current-rule-stream
                 (get-stream 
                  key 'rule-stream)))
            (put key
                 'rule-stream
                 (cons-stream 
                  rule
                  current-rule-stream)))))))

Mae'r gweithdrefnau canlynol yn diffinio sut y defnyddir mynegai'r gronfa ddata. Storir patrwm (haeriad neu gasgliad rheol) yn y tabl os yw'n dechrau â newidyn neu symbol cyson.

(define (indexable? pat)
  (or (constant-symbol? (car pat))
      (var? (car pat))))

Yr allwedd y storir patrwm oddi tani yn y tabl yw naill ai ? (os yw'n dechrau â newidyn) neu'r symbol cyson y mae'n dechrau ag ef.

(define (index-key-of pat)
  (let ((key (car pat)))
    (if (var? key) '? key)))

Defnyddir y mynegai i adfer eitemau a allai baru â phatrwm os yw'r patrwm yn dechrau â symbol cyson.

(define (use-index? pat)
  (constant-symbol? (car pat)))

Ymarfer 4.70: Beth yw diben y rhwymiadau let yn y gweithdrefnau add-assertion! ac add-rule!? Beth fyddai o'i le ar y gweithrediad canlynol o add-assertion!? Awgrym: Cofiwch ddiffiniad ffrwd anfeidrol yr unau yn 3.5.2: (define ones (cons-stream 1 ones)).
(define (add-assertion! assertion)
  (store-assertion-in-index assertion)
  (set! THE-ASSERTIONS
        (cons-stream assertion 
                     THE-ASSERTIONS))
  'ok)

4.4.4.6Gweithrediadau Ffrydiau

Mae'r system ymholi'n defnyddio ychydig o weithrediadau ffrydiau na chyflwynwyd ym Mhennod 3.

Mae Stream-append-delayed ac interleave-delayed yn union fel stream-append ac interleave (3.5.3), ac eithrio eu bod yn cymryd arg gohiriedig (fel y weithdrefn integral yn 3.5.4). Mae hyn yn gohirio dolennu mewn rhai achosion (gweler Ymarfer 4.71).

(define (stream-append-delayed s1 delayed-s2)
  (if (stream-null? s1)
      (force delayed-s2)
      (cons-stream
       (stream-car s1)
       (stream-append-delayed (stream-cdr s1)
                              delayed-s2))))

(define (interleave-delayed s1 delayed-s2)
  (if (stream-null? s1)
      (force delayed-s2)
      (cons-stream
       (stream-car s1)
       (interleave-delayed 
        (force delayed-s2)
        (delay (stream-cdr s1))))))

Mae Stream-flatmap, a ddefnyddir drwy gydol y gwerthusydd ymholiadau i fapio gweithdrefn dros ffrwd o fframiau a chyfuno'r ffrydiau o fframiau a geir, yn fersiwn ffrydiau o'r weithdrefn flatmap a gyflwynwyd ar gyfer rhestrau cyffredin yn 2.2.3. Yn wahanol i flatmap cyffredin, fodd bynnag, cronnwn y ffrydiau drwy broses gydblethu, yn hytrach na'u hatodi'n unig (gweler Ymarfer 4.72 ac Ymarfer 4.73).

(define (stream-flatmap proc s)
  (flatten-stream (stream-map proc s)))

(define (flatten-stream stream)
  (if (stream-null? stream)
      the-empty-stream
      (interleave-delayed
       (stream-car stream)
       (delay (flatten-stream
               (stream-cdr stream))))))

Mae'r gwerthusydd hefyd yn defnyddio'r weithdrefn syml ganlynol i gynhyrchu ffrwd sy'n cynnwys un elfen:

(define (singleton-stream x)
  (cons-stream x the-empty-stream))

4.4.4.7Gweithdrefnau Cystrawen Ymholiadau

Mae Type ac contents, a ddefnyddir gan qeval (4.4.4.2), yn nodi yr adnabyddir ffurf arbennig gan y symbol yn ei car. Maent yr un fath â'r gweithdrefnau type-tag ac contents yn 2.4.2, ac eithrio'r neges gwall.

(define (type exp)
  (if (pair? exp)
      (car exp)
      (error "Unknown expression TYPE"
             exp)))

(define (contents exp)
  (if (pair? exp)
      (cdr exp)
      (error "Unknown expression CONTENTS"
             exp)))

Mae'r gweithdrefnau canlynol, a ddefnyddir gan query-driver-loop (yn 4.4.4.1), yn nodi yr ychwanegir rheolau a haeriadau at y gronfa ddata drwy fynegiadau o'r ffurf (assert! ⟨rule-or-assertion⟩):

(define (assertion-to-be-added? exp)
  (eq? (type exp) 'assert!))

(define (add-assertion-body exp)
  (car (contents exp)))

Dyma'r diffiniadau cystrawen ar gyfer y ffurfiau arbennig and, or, not, ac lisp-value (4.4.4.2):

(define (empty-conjunction? exps) (null? exps))
(define (first-conjunct exps) (car exps))
(define (rest-conjuncts exps) (cdr exps))
(define (empty-disjunction? exps) (null? exps))
(define (first-disjunct exps) (car exps))
(define (rest-disjuncts exps) (cdr exps))
(define (negated-query exps) (car exps))
(define (predicate exps) (car exps))
(define (args exps) (cdr exps))

Mae'r tair gweithdrefn ganlynol yn diffinio cystrawen rheolau:

(define (rule? statement)
  (tagged-list? statement 'rule))

(define (conclusion rule) (cadr rule))

(define (rule-body rule)
  (if (null? (cddr rule))
      '(always-true)
      (caddr rule)))

Mae Query-driver-loop (4.4.4.1) yn galw query-syntax-process i drawsffurfio newidynnau patrwm yn y mynegiad, sydd â'r ffurf ?symbol, i'r fformat mewnol (? symbol). Hynny yw, cynrychiolir patrwm fel (job ?x ?y) mewn gwirionedd yn fewnol gan y system fel (job (? x) (? y)). Mae hyn yn cynyddu effeithlonrwydd prosesu ymholiadau, gan ei fod yn golygu y gall y system wirio a yw mynegiad yn newidyn patrwm drwy wirio ai'r symbol ? yw car y mynegiad, yn hytrach na gorfod tynnu nodau o'r symbol. Cyflawnir y trawsffurfiad cystrawen gan y weithdrefn ganlynol:²⁸⁵

(define (query-syntax-process exp)
  (map-over-symbols expand-question-mark exp))

(define (map-over-symbols proc exp)
  (cond ((pair? exp)
         (cons (map-over-symbols 
                proc (car exp))
               (map-over-symbols 
                proc (cdr exp))))
        ((symbol? exp) (proc exp))
        (else exp)))

(define (expand-question-mark symbol)
  (let ((chars (symbol->string symbol)))
    (if (string=? (substring chars 0 1) "?")
        (list '? (string->symbol
                  (substring
                   chars 
                   1 
                   (string-length chars))))
        symbol)))

Ar ôl trawsnewid y newidynnau fel hyn, mae'r newidynnau mewn patrwm yn restrau sy'n dechrau ag ?, a'r symbolau cyson (y mae angen eu hadnabod ar gyfer mynegeio'r gronfa ddata, 4.4.4.5) yn syml yn symbolau.

(define (var? exp) (tagged-list? exp '?))
(define (constant-symbol? exp) (symbol? exp))

Adeiledir newidynnau unigryw wrth gymhwyso rheolau (yn 4.4.4.4) drwy ddefnyddio'r gweithdrefnau canlynol. Rhif yw'r dynodwr unigryw ar gyfer cymhwysiad rheol, ac fe'i cynyddir bob tro y cymhwysir rheol.

(define rule-counter 0)

(define (new-rule-application-id)
  (set! rule-counter (+ 1 rule-counter))
  rule-counter)

(define (make-new-variable 
         var rule-application-id)
  (cons '? (cons rule-application-id
                 (cdr var))))

Pan fydd query-driver-loop yn enghreifftio'r ymholiad er mwyn argraffu'r ateb, mae'n trosi unrhyw newidynnau patrwm rhydd yn ôl i'r ffurf gywir ar gyfer argraffu, gan ddefnyddio

(define (contract-question-mark variable)
  (string->symbol
   (string-append "?"
     (if (number? (cadr variable))
         (string-append
          (symbol->string (caddr variable))
          "-"
          (number->string (cadr variable)))
         (symbol->string (cadr variable))))))

4.4.4.8Fframiau a Rhwymiadau

Cynrychiolir fframiau fel rhestrau o rwymiadau, sef parau newidyn-gwerth:

(define (make-binding variable value)
  (cons variable value))

(define (binding-variable binding)
  (car binding))

(define (binding-value binding)
  (cdr binding))

(define (binding-in-frame variable frame)
  (assoc variable frame))

(define (extend variable value frame)
  (cons (make-binding variable value) frame))

Ymarfer 4.71: Mae Louis Reasoner yn pendroni pam y gweithredir y gweithdrefnau simple-query ac disjoin (4.4.4.2) drwy ddefnyddio gweithrediadau delay penodol, yn hytrach na'u diffinio fel a ganlyn:
(define (simple-query 
         query-pattern frame-stream)
  (stream-flatmap
   (lambda (frame)
     (stream-append
      (find-assertions query-pattern frame)
      (apply-rules query-pattern frame)))
   frame-stream))

(define (disjoin disjuncts frame-stream)
  (if (empty-disjunction? disjuncts)
      the-empty-stream
      (interleave
       (qeval (first-disjunct disjuncts)
              frame-stream)
       (disjoin (rest-disjuncts disjuncts)
                frame-stream))))
A allwch roi enghreifftiau o ymholiadau lle byddai'r diffiniadau symlach hyn yn arwain at ymddygiad annymunol?

Ymarfer 4.72: Pam mae disjoin ac stream-flatmap yn cydblethu'r ffrydiau yn hytrach na'u hatodi'n unig? Rhowch enghreifftiau sy'n dangos pam mae cydblethu yn gweithio'n well. (Awgrym: Pam y defnyddion ni interleave yn 3.5.3?)

Ymarfer 4.73: Pam mae flatten-stream yn defnyddio delay yn benodol? Beth fyddai o'i le ar ei ddiffinio fel a ganlyn:
(define (flatten-stream stream)
  (if (stream-null? stream)
      the-empty-stream
      (interleave (stream-car stream)
                  (flatten-stream 
                   (stream-cdr stream)))))

Ymarfer 4.74: Mae Alyssa P. Hacker yn cynnig defnyddio fersiwn symlach o stream-flatmap yn negate, lisp-value, ac find-assertions. Mae'n sylwi bod y weithdrefn a fapir dros y ffrwd fframiau yn yr achosion hyn bob amser yn cynhyrchu naill ai'r ffrwd wag neu ffrwd un elfen, felly nid oes angen cydblethu wrth gyfuno'r ffrydiau hyn.
Llenwch y mynegiadau coll yn rhaglen Alyssa.
(define (simple-stream-flatmap proc s)
  (simple-flatten (stream-map proc s)))

(define (simple-flatten stream)
  (stream-map ⟨??⟩
              (stream-filter ⟨??⟩ 
                             stream)))
A yw ymddygiad y system ymholiadau yn newid os newidiwn hi fel hyn?

Ymarfer 4.75: Gweithredwch ffurf arbennig newydd o'r enw unique ar gyfer yr iaith ymholiadau. Dylai Unique lwyddo os oes un eitem yn union yn y gronfa ddata sy'n bodloni ymholiad penodedig. Er enghraifft,
(unique (job ?x (computer wizard)))
dylai argraffu'r ffrwd un eitem
(unique (job (Bitdiddle Ben)
             (computer wizard)))
gan mai Ben yw'r unig ddewin cyfrifiadurol, a
(unique (job ?x (computer programmer)))
dylai argraffu'r ffrwd wag, gan fod mwy nag un rhaglennydd cyfrifiadurol. Ar ben hynny,
(and (job ?x ?j) 
     (unique (job ?anyone ?j)))
dylai restru'r holl swyddi a lenwir gan un person yn unig, a'r bobl sy'n eu llenwi.

Mae dwy ran i weithredu unique. Y gyntaf yw ysgrifennu gweithdrefn sy'n trin y ffurf arbennig hon, a'r ail yw gwneud i qeval ddethol y weithdrefn honno. Mae'r ail ran yn ddibwys, gan fod qeval yn dethol gweithdrefnau mewn ffordd a gyfarwyddir gan ddata. Os mai uniquely-asserted yw enw'ch gweithdrefn, y cyfan sydd angen ichi ei wneud yw
(put 'unique 'qeval uniquely-asserted)
a bydd qeval yn dethol y weithdrefn hon ar gyfer pob ymholiad y mae ei type (car) yn symbol unique.

Y broblem wirioneddol yw ysgrifennu'r weithdrefn uniquely-asserted. Dylai hon gymryd contents (cdr) yr ymholiad unique fel mewnbwn, ynghyd â ffrwd o fframiau. Ar gyfer pob ffrâm yn y ffrwd, dylai ddefnyddio qeval i ganfod ffrwd yr holl estyniadau i'r ffrâm sy'n bodloni'r ymholiad a roddwyd. Dylid dileu unrhyw ffrwd nad yw'n cynnwys un eitem yn union. Dylid dychwelyd y ffrydiau sy'n weddill i'w cronni mewn un ffrwd fawr sy'n ganlyniad yr ymholiad unique. Mae hyn yn debyg i weithrediad y ffurf arbennig not.

Profwch eich gweithrediad drwy ffurfio ymholiad sy'n rhestru'r holl bobl sy'n goruchwylio un person yn union.

Ymarfer 4.76: Mae ein gweithrediad o and fel cyfuniad cyfres o ymholiadau (Ffigur 4.5) yn gain, ond mae'n aneffeithlon oherwydd, wrth brosesu ail ymholiad yr and, rhaid inni sganio'r gronfa ddata ar gyfer pob ffrâm a gynhyrchir gan yr ymholiad cyntaf. Os oes $n$ elfen yn y gronfa ddata, a bod ymholiad nodweddiadol yn cynhyrchu nifer o fframiau allbwn sy'n gyfrannol ag $n$ (dyweder $n / k$ ), yna bydd sganio'r gronfa ddata ar gyfer pob ffrâm a gynhyrchir gan yr ymholiad cyntaf yn gofyn am $n^{2} / k$ galwad i'r parydd patrymau. Dull arall fyddai prosesu dau gymal yr and ar wahân, ac yna chwilio am bob pâr o fframiau allbwn sy'n gydnaws. Os yw pob ymholiad yn cynhyrchu $n / k$ ffrâm allbwn, mae hyn yn golygu bod rhaid inni gyflawni $n^{2} / k^{2}$ gwiriad cydnawsedd—llai na nifer y pariadau sydd eu hangen yn ein dull presennol o ffactor o $k$ .

Dyfeisiwch weithrediad o and sy'n defnyddio'r strategaeth hon. Rhaid ichi weithredu gweithdrefn sy'n cymryd dwy ffrâm fel mewnbynnau, yn gwirio a yw'r rhwymiadau yn y fframiau yn gydnaws, ac, os ydynt, yn cynhyrchu ffrâm sy'n cyfuno'r ddwy set o rwymiadau. Mae'r gweithrediad hwn yn debyg i uno patrymau.

Ymarfer 4.77: Yn 4.4.3 gwelsom y gall not ac lisp-value beri i'r iaith ymholiadau roi atebion “anghywir” os cymhwysir y gweithrediadau hidlo hyn i fframiau lle nad yw newidynnau wedi'u rhwymo. Dyfeisiwch ffordd o gywiro'r diffyg hwn. Un syniad yw cyflawni'r hidlo mewn modd “gohiriedig” drwy atodi “addewid” i hidlo i'r ffrâm, a gyflawnir dim ond pan fydd digon o newidynnau wedi'u rhwymo i wneud y gweithrediad yn bosibl. Gallem aros i hidlo nes bod yr holl weithrediadau eraill wedi'u cyflawni. Fodd bynnag, er mwyn effeithlonrwydd, hoffem hidlo cyn gynted â phosibl er mwyn lleihau nifer y fframiau canolradd a gynhyrchir.

Ymarfer 4.78: Ailgynlluniwch yr iaith ymholiadau fel rhaglen an-benderfyniaethol i'w gweithredu gan ddefnyddio gwerthusydd 4.3, yn hytrach nag fel proses ffrydiau. Yn y dull hwn, bydd pob ymholiad yn cynhyrchu un ateb (yn hytrach na ffrwd yr holl atebion) a gall y defnyddiwr deipio try-again i weld mwy o atebion. Dylech ganfod bod chwilio an-benderfyniaethol a gwrthgilio yn cwmpasu llawer o'r peirianwaith a adeiladwyd gennym yn yr adran hon. Fodd bynnag, mae'n debyg y byddwch hefyd yn canfod bod gwahaniaethau cynnil rhwng ymddygiad eich iaith ymholiadau newydd a'r un a weithredwyd yma. A allwch ganfod enghreifftiau sy'n dangos y gwahaniaeth hwn?

Ymarfer 4.79: Pan weithredon ni'r gwerthusydd Lisp yn 4.1, gwelsom sut i ddefnyddio amgylcheddau lleol i osgoi gwrthdaro enwau rhwng paramedrau gweithdrefnau. Er enghraifft, wrth werthuso
(define (square x) 
  (* x x))

(define (sum-of-squares x y)
  (+ (square x) (square y)))

(sum-of-squares 3 4)
nid oes dryswch rhwng yr x yn square a'r x yn sum-of-squares, oherwydd gwerthuswn gorff pob gweithdrefn mewn amgylchedd a adeiledir yn arbennig i gynnwys rhwymiadau ar gyfer y newidynnau lleol. Yn y system ymholiadau, defnyddion ni strategaeth wahanol i osgoi gwrthdaro enwau wrth gymhwyso rheolau. Bob tro y cymhwyswn reol, rydym yn ailenwi'r newidynnau ag enwau newydd y gwarentir eu bod yn unigryw. Y strategaeth gyfatebol ar gyfer y gwerthusydd Lisp fyddai dileu amgylcheddau lleol ac, yn syml, ailenwi'r newidynnau yng nghorff gweithdrefn bob tro y cymhwyswn y weithdrefn.

Gweithredwch ddull cymhwyso rheolau ar gyfer yr iaith ymholiadau sy'n defnyddio amgylcheddau yn hytrach nag ailenwi. Gwelwch a allwch adeiladu ar eich strwythur amgylcheddau i greu lluniadau yn yr iaith ymholiadau ar gyfer trin systemau mawr, megis cyfatebiaeth rheolau i weithdrefnau â strwythur blociau. A allwch gysylltu dim o hyn â'r broblem o wneud diddwythiadau mewn cyd-destun (e.e., “Pe bawn yn tybio bod $P$ yn wir, yna byddwn yn gallu diddwytho $A$ ac $B$ .”) fel dull o ddatrys problemau? (Mae'r broblem hon yn benagored. Mae'n debyg bod ateb da yn werth Ph.D.)

Troednodiadau

²⁶² Mae rhaglennu rhesymeg wedi tyfu o hanes hir o ymchwil i brofi theoremau'n awtomatig. Ychydig iawn y gallai rhaglenni profi theoremau cynnar ei gyflawni, oherwydd byddent yn chwilio'n drwyadl drwy ofod yr holl brofion posibl. Y datblygiad mawr a wnaeth chwiliad o'r fath yn ymarferol oedd darganfod yr algorithm uno patrymau a'r egwyddor cydraniad (resolution principle) yn gynnar yn y 1960au (Robinson 1965). Defnyddiwyd cydraniad, er enghraifft, gan Green a Raphael (1968) (gweler hefyd Green 1969) fel sail i system ddiddwythol ar gyfer ateb cwestiynau. Yn ystod y rhan fwyaf o'r cyfnod hwn, canolbwyntiai ymchwilwyr ar algorithmau y gwarentir eu bod yn canfod prawf os oes un yn bodoli. Roedd algorithmau o'r fath yn anodd eu rheoli a'u cyfeirio tuag at brawf. Sylweddolodd Hewitt (1969) fod modd cyfuno strwythur rheoli iaith raglennu â gweithrediadau system trin rhesymeg, gan arwain at y gwaith mewn chwilio awtomatig a grybwyllwyd yn 4.3.1 (Troednodyn 250). Ar yr un pryd â hyn, roedd Colmerauer, ym Marseille, yn datblygu systemau seiliedig ar reolau ar gyfer trin iaith naturiol (gweler Colmerauer et al. 1973). Dyfeisiodd iaith raglennu o'r enw Prolog i gynrychioli'r rheolau hynny. Sylweddolodd Kowalski (1973; 1979), yng Nghaeredin, y gellid dehongli gweithredu rhaglen Prolog fel profi theoremau (gan ddefnyddio techneg profi o'r enw cydraniad llinol cymalau Horn). Arweiniodd uno'r ddau drywydd olaf at y mudiad rhaglennu rhesymeg. Felly, wrth briodoli clod am ddatblygiad rhaglennu rhesymeg, gall y Ffrancwyr gyfeirio at darddiad Prolog ym Mhrifysgol Marseille, tra gall y Prydeinwyr bwysleisio'r gwaith ym Mhrifysgol Caeredin. Yn ôl pobl yn MIT, datblygwyd rhaglennu rhesymeg gan y grwpiau hyn wrth geisio deall yr hyn yr oedd Hewitt yn ei ddweud yn ei draethawd Ph.D. disglair ond anhreiddiadwy. Am hanes rhaglennu rhesymeg, gweler Robinson 1983.

²⁶³ I weld y cyfatebiaeth rhwng y rheolau a'r weithdrefn, gadewch i x yn y weithdrefn (lle mae x yn anwag) gyfateb i (cons u v) yn y rheol. Yna mae z yn y rheol yn cyfateb i append (cdr x) ac y.

²⁶⁴ Yn sicr, nid yw hyn yn rhyddhau'r defnyddiwr rhag yr holl broblem o sut i gyfrifo'r ateb. Mae llawer o setiau gwahanol o reolau sy'n gyfwerth yn fathemategol ar gyfer ffurfio'r berthynas append, a dim ond rhai ohonynt y gellir eu troi'n fecanweithiau effeithiol ar gyfer cyfrifo i unrhyw gyfeiriad. Yn ogystal, weithiau nid yw gwybodaeth am “beth sydd” yn rhoi unrhyw gliw ynghylch “sut i” gyfrifo ateb. Er enghraifft, ystyriwch y broblem o gyfrifo'r $y$ fel bod $y^{2} = x$ .

²⁶⁵ Cyrhaeddodd diddordeb mewn rhaglennu rhesymeg ei uchafbwynt ar ddechrau'r 80au pan gychwynnodd llywodraeth Japan brosiect uchelgeisiol i adeiladu cyfrifiaduron cyflym iawn wedi'u hoptimeiddio i redeg ieithoedd rhaglennu rhesymeg. Bwriadwyd mesur cyflymder cyfrifiaduron o'r fath mewn LIPS (Logical Inferences Per Second, casgliadau rhesymegol yr eiliad) yn hytrach na'r FLOPS arferol (FLoating-point Operations Per Second, gweithrediadau pwynt arnofiol yr eiliad). Er i'r prosiect lwyddo i ddatblygu caledwedd a meddalwedd fel y bwriadwyd yn wreiddiol, symudodd y diwydiant cyfrifiaduron rhyngwladol i gyfeiriad gwahanol. Gweler Feigenbaum a Shrobe 1993 am werthusiad cyffredinol o'r prosiect Japaneaidd. Mae'r gymuned rhaglennu rhesymeg hefyd wedi symud ymlaen i ystyried rhaglennu perthynol wedi'i seilio ar dechnegau heblaw paru patrymau syml, megis y gallu i drin cyfyngiadau rhifiadol fel y rhai a ddangoswyd yn system lledaenu cyfyngiadau 3.3.5.

²⁶⁶ Mae hyn yn defnyddio'r nodiant cynffon ddotiog a gyflwynwyd yn Ymarfer 2.20.

²⁶⁷ Mewn gwirionedd, dim ond ar gyfer achosion syml y mae'r disgrifiad hwn o not yn ddilys. Mae gwir ymddygiad not yn fwy cymhleth. Byddwn yn archwilio hynodion not yn 4.4.2 ac 4.4.3.

²⁶⁸ Dylid defnyddio Lisp-value dim ond i gyflawni gweithrediad nad yw ar gael yn yr iaith ymholiadau. Yn benodol, ni ddylid ei ddefnyddio i brofi hafaledd (gan mai dyna y bwriedir i'r paru yn yr iaith ymholiadau ei wneud) nac anhafaledd (gan y gellir gwneud hynny â'r rheol same a ddangosir isod).

²⁶⁹ Sylwch nad oes angen same arnom er mwyn gwneud dau beth yr un peth: Defnyddiwn yr un newidyn patrwm ar gyfer pob un—i bob pwrpas, un peth sydd gennym yn lle dau beth yn y lle cyntaf. Er enghraifft, gweler ?town yn y rheol lives-near ac ?middle-manager yn y rheol wheel isod. Mae Same yn ddefnyddiol pan fyddwn am orfodi dau beth i fod yn wahanol, megis ?person-1 ac ?person-2 yn y rheol lives-near. Er bod defnyddio'r un newidyn patrwm mewn dwy ran o ymholiad yn gorfodi'r un gwerth i ymddangos yn y ddau le, nid yw defnyddio newidynnau patrwm gwahanol yn gorfodi gwerthoedd gwahanol i ymddangos. (Gall y gwerthoedd a aseinir i newidynnau patrwm gwahanol fod yr un fath neu'n wahanol.)

²⁷⁰ Byddwn hefyd yn caniatáu rheolau heb gyrff, fel yn same, a byddwn yn dehongli rheol o'r fath i olygu bod casgliad y rheol yn cael ei fodloni gan unrhyw werthoedd i'r newidynnau.

²⁷¹ Gan fod paru fel arfer yn ddrud iawn, hoffem osgoi cymhwyso'r parydd llawn i bob elfen o'r gronfa ddata. Trefnir hyn fel arfer drwy rannu'r broses yn baru bras cyflym a'r paru terfynol. Mae'r paru bras yn hidlo'r gronfa ddata i gynhyrchu set fach o ymgeiswyr ar gyfer y paru terfynol. Gyda gofal, gallwn drefnu ein cronfa ddata fel y gellir gwneud rhywfaint o'r gwaith paru bras wrth adeiladu'r gronfa ddata yn hytrach na phan fyddwn am ddethol yr ymgeiswyr. Gelwir hyn yn fynegeio'r gronfa ddata. Mae maes technolegol helaeth wedi tyfu o amgylch cynlluniau mynegeio cronfeydd data. Mae ein gweithrediad ni, a ddisgrifir yn 4.4.4, yn cynnwys ffurf syml iawn o optimeiddiad o'r fath.

²⁷² Ond nid yw'r math hwn o ffrwydrad esbonyddol yn gyffredin mewn ymholiadau and oherwydd bod yr amodau ychwanegol yn tueddu i leihau nifer y fframiau a gynhyrchir yn hytrach na'i gynyddu.

²⁷³ Mae llenyddiaeth helaeth ar systemau rheoli cronfeydd data sy'n ymwneud â sut i drin ymholiadau cymhleth yn effeithlon.

²⁷⁴ Mae gwahaniaeth cynnil rhwng y gweithrediad hwn o not drwy hidlo ac ystyr arferol not mewn rhesymeg fathemategol. Gweler 4.4.3.

²⁷⁵ Mewn paru patrymau unochrog, mae'r holl hafaliadau sy'n cynnwys newidynnau patrwm yn eglur ac eisoes wedi'u datrys ar gyfer yr anhysbysyn (y newidyn patrwm).

²⁷⁶ Ffordd arall o feddwl am uno patrymau yw ei fod yn cynhyrchu'r patrwm mwyaf cyffredinol sy'n arbenigiad o'r ddau batrwm mewnbwn. Hynny yw, canlyniad uno (?x a) ac ((b ?y) ?z) yw ((b ?y) a), a chanlyniad uno (?x a ?y) ac (?y ?z a), a drafodwyd uchod, yw (a a a). Ar gyfer ein gweithrediad ni, mae'n fwy cyfleus meddwl am ganlyniad uno fel ffrâm yn hytrach na phatrwm.

²⁷⁷ Gan fod uno patrymau yn gyffredinoliad o baru, gallem symleiddio'r system drwy ddefnyddio'r unydd i gynhyrchu'r ddwy ffrwd. Fodd bynnag, mae trin yr achos hawdd â'r parydd syml yn dangos sut y gall paru (yn hytrach nag uno llawn) fod yn ddefnyddiol ynddo'i hun.

²⁷⁸ Y rheswm y defnyddiwn ffrydiau (yn hytrach na rhestrau) o fframiau yw y gall cymhwyso rheolau'n ddychweliadol gynhyrchu nifer anfeidrol o werthoedd sy'n bodloni ymholiad. Mae'r gwerthuso gohiriedig sydd wedi'i ymgorffori mewn ffrydiau yn hanfodol yma: Bydd y system yn argraffu ymatebion fesul un wrth iddynt gael eu cynhyrchu, ni waeth a oes nifer feidraidd neu anfeidrol o ymatebion.

²⁷⁹ Nid haeriad dibwys yw dweud bod dull casglu penodol yn ddilys. Rhaid profi, os dechreuir â rhagosodiadau gwir, mai dim ond casgliadau gwir y gellir eu deillio. Y dull casglu a gynrychiolir gan gymhwyso rheolau yw modus ponens, y dull casglu cyfarwydd sy'n dweud, os yw $A$ yn wir ac os yw A yn ymhlygu B yn wir, yna gallwn gasglu bod $B$ yn wir.

²⁸⁰ Rhaid inni amodi'r datganiad hwn drwy gytuno ein bod, wrth sôn am y “casglu” a gyflawnir gan raglen resymeg, yn tybio bod y cyfrifiad yn gorffen. Yn anffodus, mae hyd yn oed y datganiad amodol hwn yn anwir ar gyfer ein gweithrediad ni o'r iaith ymholiadau (ac mae hefyd yn anwir ar gyfer rhaglenni Prolog a'r rhan fwyaf o ieithoedd rhaglennu rhesymeg cyfredol eraill) oherwydd ein defnydd o not ac lisp-value. Fel y disgrifiwn isod, nid yw'r not a weithredir yn yr iaith ymholiadau bob amser yn gyson ag not rhesymeg fathemategol, ac mae lisp-value yn cyflwyno cymhlethdodau ychwanegol. Gallem weithredu iaith sy'n gyson â rhesymeg fathemategol drwy dynnu not ac lisp-value o'r iaith yn unig a chytuno i ysgrifennu rhaglenni gan ddefnyddio ymholiadau syml, and, ac or yn unig. Fodd bynnag, byddai hyn yn cyfyngu'n fawr ar bŵer mynegiannol yr iaith. Un o brif bynciau ymchwil mewn rhaglennu rhesymeg yw canfod ffyrdd o sicrhau mwy o gysondeb â rhesymeg fathemategol heb aberthu pŵer mynegiannol i raddau gormodol.

²⁸¹ Nid problem gyda'r rhesymeg yw hon, ond gyda'r dehongliad gweithdrefnol o'r rhesymeg a ddarperir gan ein dehonglydd. Gallem ysgrifennu dehonglydd na fyddai'n mynd i ddolen yma. Er enghraifft, gallem rifo'r holl brofion y gellir eu deillio o'n haeriadau a'n rheolau mewn trefn lled yn gyntaf yn hytrach na dyfnder yn gyntaf. Fodd bynnag, mae system o'r fath yn ei gwneud yn anoddach manteisio ar drefn diddwythiadau yn ein rhaglenni. Disgrifir un ymgais i ymgorffori rheolaeth soffistigedig mewn rhaglen o'r fath yn deKleer et al. 1977. Techneg arall, nad yw'n arwain at broblemau rheoli mor ddifrifol, yw cynnwys gwybodaeth arbennig, megis synwyryddion ar gyfer mathau penodol o ddolenni (Ymarfer 4.67). Fodd bynnag, ni all fod cynllun cyffredinol sy'n atal system yn ddibynadwy rhag dilyn llwybrau anfeidrol wrth gyflawni diddwythiadau. Dychmygwch reol ddrygionus ar ffurf “I ddangos bod $P (x)$ yn wir, dangoswch fod $P (f (x))$ yn wir,” ar gyfer rhyw ffwythiant $f$ wedi'i ddewis yn addas.

²⁸² Ystyriwch yr ymholiad (not (baseball-fan (Bitdiddle Ben))). Mae'r system yn canfod nad yw (baseball-fan (Bitdiddle Ben)) yn y gronfa ddata, felly nid yw'r ffrâm wag yn bodloni'r patrwm ac ni chaiff ei hidlo allan o'r ffrwd gychwynnol o fframiau. Canlyniad yr ymholiad felly yw'r ffrâm wag, a ddefnyddir i enghreifftio'r ymholiad mewnbwn i gynhyrchu (not (baseball-fan (Bitdiddle Ben))).

²⁸³ Ceir trafodaeth a chyfiawnhad o'r driniaeth hon o not yn yr erthygl gan Clark (1978).

²⁸⁴ Yn gyffredinol, byddai uno ?y â mynegiad sy'n cynnwys ?y yn gofyn inni allu canfod pwynt sefydlog i'r hafaliad ?y = ⟨expression involving ?y⟩. Weithiau mae'n bosibl ffurfio mynegiad yn gystrawennol sy'n ymddangos fel pe bai'n ddatrysiad. Er enghraifft, ymddengys fod gan ?y = (f ?y) y pwynt sefydlog (f (f (f … ))), y gallwn ei gynhyrchu drwy ddechrau â'r mynegiad (f ?y) ac amnewid ?y ag (f ?y) dro ar ôl tro. Yn anffodus, nid oes pwynt sefydlog ystyrlon i bob hafaliad o'r fath. Mae'r materion sy'n codi yma yn debyg i faterion trin cyfresi anfeidrol mewn mathemateg. Er enghraifft, gwyddom mai 2 yw datrysiad yr hafaliad $y = 1 + y / 2$ . Mae dechrau â'r mynegiad $1 + y / 2$ ac amnewid $y$ ag $1 + y / 2$ dro ar ôl tro yn rhoi $2 = y = 1 + \frac{y}{2} = 1 + \frac{1}{2} (1 + \frac{y}{2}) = 1 + \frac{1}{2} + \frac{y}{4} = \dots,$ sy'n arwain at $2 = 1 + \frac{1}{2} + \frac{1}{4} + \frac{1}{8} + \dots .$ Fodd bynnag, os ceisiwn yr un driniaeth gan ddechrau â'r sylw mai $- 1$ yw datrysiad yr hafaliad $y = 1 + 2 y$ , cawn $- 1 = y = 1 + 2 y = 1 + 2 (1 + 2 y) = 1 + 2 + 4 y = \dots,$ sy'n arwain at $- 1 = 1 + 2 + 4 + 8 + \dots .$ Er bod y triniaethau ffurfiol a ddefnyddir i ddeillio'r ddau hafaliad hyn yn unfath, mae'r canlyniad cyntaf yn haeriad dilys ynghylch cyfresi anfeidrol ond nid yw'r ail. Yn yr un modd, ar gyfer ein canlyniadau uno, gall rhesymu â mynegiad mympwyol a adeiladwyd yn gystrawennol arwain at wallau.

²⁸⁵ Mae'r rhan fwyaf o systemau Lisp yn rhoi'r gallu i'r defnyddiwr addasu'r weithdrefn read arferol i gyflawni trawsnewidiadau o'r fath drwy ddiffinio nodau macro'r darllenydd. Ymdrinnir â mynegiadau a ddyfynnir yn y ffordd hon eisoes: Mae'r darllenydd yn trosi 'expression yn (quote expression) yn awtomatig cyn i'r gwerthusydd ei weld. Gallem drefnu trawsnewid ?expression yn (? expression) yn yr un ffordd; fodd bynnag, er eglurder rydym wedi cynnwys y weithdrefn trawsnewid yma yn benodol.

Mae Expand-question-mark ac contract-question-mark yn defnyddio sawl gweithdrefn ag string yn eu henwau. Gweithdrefnau cyntefig Scheme yw'r rhain.

4.4 Rhaglennu Rhesymegol

4.4.1Adalw Gwybodaeth drwy Ddiddwytho

Cronfa ddata enghreifftiol

Ymholiadau syml

Ymholiadau cyfansawdd

Rheolau

Rhesymeg fel rhaglenni

4.4.2Sut Mae'r System Ymholi'n Gweithio

Paru patrymau

Ffrydiau o fframiau

Ymholiadau cyfansawdd

Uno patrymau

Cymhwyso rheolau

Ymholiadau syml

Y gwerthusydd ymholi a'r ddolen yrru

4.4.3Ai Rhesymeg Fathemategol yw Rhaglennu Rhesymegol?

Dolenni anfeidraidd

Problemau gydag not

4.4.4Gweithredu'r System Ymholi

4.4.4.1Y Ddolen Yrru ac Enghreifftio

4.4.4.2Y Gwerthusydd

Ymholiadau syml

Ymholiadau cyfansawdd

Hidlyddion

4.4.4.3Canfod Haeriadau drwy Baru Patrymau

Patrymau â chynffonnau dotiog

4.4.4.4Rheolau ac Uno

4.4.4.5Cynnal y Gronfa Ddata

4.4.4.6Gweithrediadau Ffrydiau

4.4.4.7Gweithdrefnau Cystrawen Ymholiadau

4.4.4.8Fframiau a Rhwymiadau

Troednodiadau

Problemau gydag `not`