constructoren, UNA, DCA

Filosofie:

Structuren en Theorieen mergen. Een structuur zal een theorie zijn die aan bepaalde voorwaarden voldoet. Welke voorwaarden zullen we nog zien. Een van de effecten is dat het onderscheid tussen domeinelement en constante wegvalt.

Er zijn twee aspecten:

1) UNA

het feit dat er een hoop identifiers in een theorie kunnen voorkomen, die verschillend zijn

we willen niet altijd alle identifiers van elk type moeten opsommen
we willen kunnen aangeven dat ze allemaal verschillende objecten voorstellen of juist niet.
we willen kunnen een verzameling van functies en constante als een verzameling van constructoren definieren

het type van de identifiers wordt afgeleid door type inferentie. (dit is niet triviaal in geval van order sorted types) We kunnen ook expliciete definities geven voor type.

Per theorie/structuur stellen we een default: verschillende identifiers/ potentieel zelfde objecten

We verandere de default door in de theorie op te nemen: UNA : default 1 voor alle identifiers van alle types

Meer verfijnder commando's: UNA(t) : default UNA voor alle identifiers van type t UNA({nil/0:,list(A,Lijst):Lijst}) : nil en list zijn samen constructoren.

2) DCA

Daarmee willen we al dan niet een of meer verschillende types sluiten.

Ik zou verschillende mechanismes voorzien

DCA: sluit alle types: er zijn geen andere objecten dan diegene die door termen voorgesteld worden
DCA(t): sluit type t
DCA(t,{nil/0,list(A,Lijst):Lijst): t bevat geen andere objecten dan diegene die door constanten uit nil en listconstructor list geconstrueerd kunnen worden uit type A.
Een expliciete definitie van type t {! x: t(x) <- ...} of eventueel door opsomming t = { ... }

Wat is een structuur dan? het is een theorie van de vorm

Theory (met of zonder voc) { UNA t1 = {} t2 = {} ... P1 = { ..} ... }

Comments (2)