Harrop formel
I intuitionistisk logik är Harrop -formlerna , uppkallade efter Ronald Harrop, den klass av formler som induktivt definieras enligt följande:
- Atomformler är Harrop, inklusive falskhet (⊥);
- är Harrop förutsatt att och är;
- är Harrop för vilken välformad formel som helst ;
- är Harrop förutsatt att är, och är vilken välformad formel som helst;
- är Harrop förutsatt att är.
Genom att utesluta disjunktion och existentiell kvantifiering (förutom i antecedenten av implikation) undviks icke-konstruktiva predikat, vilket har fördelar för datorimplementering. Ur en konstruktivistisk synvinkel är Harrops formler "väluppfostrade". Till exempel, i Heyting-arithmetic , uppfyller Harrop-formler en klassisk ekvivalens som vanligtvis inte är uppfylld i konstruktiv logik:
Harrop formler introducerades runt 1956 av Ronald Harrop och oberoende av Helena Rasiowa . Variationer av det grundläggande konceptet används inom olika grenar av konstruktiv matematik och logikprogrammering .
Ärftliga Harrop-formler och logikprogrammering
En mer komplex definition av ärftliga Harrop-formler används i logisk programmering som en generalisering av Horn-satser , och utgör grunden för språket λProlog . Ärftliga Harrop-formler definieras i termer av två (ibland tre) rekursiva formler. I en formulering:
- Stela atomformler, dvs konstanter eller formler , är ärftliga Harrop ;
- är ärftlig Harrop förutsatt att och är;
- är ärftlig Harrop förutsatt att är;
- är ärftlig Harrop förutsatt att är styvt atomär och är en G -formel.
G -formler definieras enligt följande:
- Atomformler är G -formler, inklusive sanning(⊤);
- är en G -formel förutsatt att och är;
- är en G -formel förutsatt att och är;
- är en G -formel förutsatt att är;
- är en G -formel förutsatt att är;
- är en G -formel förutsatt att är, och är ärftlig Harrop.
