Overleg:Beweren en bewijzen/het werk/oefenpagina/familietoestanden
Definition broerVan (x:M) (y:M) := ∃ z:M, ouderVan z x ∧ ouderVan z y ∧ isMan x , mijn vraag hierbij is: horen x en y niet de ouder van z te zijn? en hoort z dan niet de man te zijn?
| Ik lees dit als: x is een broer van y als er een z is, z is de ouder van x en z is de ouder van y, en x is een man. X is immers een broer van Y als ze een gemeenschappelijke ouder Z hebben, en X een man is. Lijkt mij prima geformuleerd zo. | ||
| Koray Yanik → Beweren en bewijzen | Remove this comment when resolved! | |
| Het veld "type" in de domeinmodel vind ik onduidelijk (het onderste gedeelte). Weet iemand waar de verschillende letters voor staan? De 'M' staat wel uitgelegd, maar waarvoor staan de andere letters? |  |
|
| Tolga Gök → Beweren en bewijzen | Remove this comment when resolved! | |
| Ik heb een vraagje over het schema op de werk pagina. Waar kan ik namelijk vinden wat voor een type een definitie is? Ik heb al even rondgekeken op de wiki, maar heb niks kunnen vinden. Kan iemand mij zeggen waar ik het kan vinden of het aan mij uitleggen? |  |
|
| Idzard Stoker → Beweren en bewijzen | Remove this comment when resolved! | |
| Ik heb hieronder wat uitleg over typeringen toegevoegd in de hoop de vragen te beantwoorden. | ||
| Pol van Aubel → Beweren en bewijzen | Remove this comment when resolved! | |
Met het risico dit te complex uit te leggen... Dit komt allemaal uit de wiskundige functietheorie. Een predikaat als "isMan" is een functie die, gegeven een element uit de verzameling van alle levende en dode mensen (M), je een waarde teruggeeft uit de verzameling Boolse waarden ({Waar, Onwaar}, wat ook wel wordt weergegeven als {1, 0} of {True, False} afhankelijk van je voorkeur. Afgekort is dit B.) die bij dat element hoort. "isMan Beatrix" levert Onwaar, "isMan Willem-Alexander" levert Waar. Het type van een functie beschrijft uit welke verzameling deze functie elementen verwacht en uit welke verzameling de bijbehorende elementen komen. Het type van de functie isMan is dus "M → B".
Als je een letter tegenkomt waarvan je niet weet wat hij betekent, moet je bovenaan in het domeinmodel zoeken naar de verzameling die bij die letter hoort.
Er zijn ook functies die meerdere argumenten verwachten alvorens ze een resultaat teruggeven. Dit kunnen predikaten zijn, maar ook complexere definities die intern gebruik maken van andere predikaten (eigenlijk kun je zelfs hele beweringen zien als functies). Neem als voorbeeld het predikaat ouderVan. Dit is een predikaat dat aangeeft of de persoon die je als eerste argument geeft ouder is van de persoon die je als tweede argument geeft. Oftewel, dit is een functie die, gegeven een element uit M en een element uit M, het bijbehorende element uit de verzameling B teruggeeft. Nu zijn er meerdere manieren om dit te noteren, mensen die discrete wiskunde gevolgd hebben zal de notatie "(M x M) → B" bekend voorkomen. Echter, bij beweren en bewijzen wordt een techniek gebruikt die "currying" heet, en die resulteert in de notatie "M → M → B". Het afleiden van het type van een wat complexere definitie is dus helemaal niet zo moeilijk: Alle definities eindigen bij ons tot nu toe sowieso in een Boolse waarde, dus in "→ B". Je bepaalt uit welke verzameling de elementen die je als argumenten meegeeft komen, en die zet je er vervolgens in de juiste volgorde voor. Het type van "Definition broerVan (x:M) (y:M) := ? z:M, ouderVan z x ? ouderVan z y ? isMan x." is dus M → M → B
Als je dit afdoende vindt om je vraag te beantwoorden kun je nu stoppen met lezen, hieronder volgt alleen nog wat complexere theorie.
Currying komt in feite op het volgende neer: Een functie die meerdere argumenten neemt is eigenlijk een "ketting" van functies die elk één argument nemen en daarbij een nieuwe functie teruggeven die ook weer één argument neemt. Alleen de laatste functie in deze ketting produceert het daadwerkelijke resultaat.
De "→" is rechts associatief, dus je moet "M → M → B" lezen als "M → (M → B)". ouderVan is dus een functie die als enkel argument elementen accepteert uit de verzameling M. Het resultaat dat dan teruggegeven wordt komt uit de verzameling (M → B). Deze verzameling is een verzameling functies met type "M → B": functies die, gegeven een enkel argument uit de verzameling M, een boolse waarde teruggeven. Dus als ik de functie "ouderVan" een element uit M geef, bijvoorbeeld Beatrix, dan krijg ik een functie die een enkel element uit M als argument neemt en mij vertelt of Beatrix een ouder is van dat element. Deze functie zal dus alle kinderen van Beatrix aan "Waar" koppelen en alle andere mensen aan "Onwaar". Omdat deze functies als ketting uitgevoerd worden merk je hier (nog?) niets van in predikaatlogica, maar als je volgend jaar aan de slag gaat met functioneel programmeren krijg je hier nog wel mee te maken.
-- Pol Van Aubel
|
Ik wil het even over der volgende definitie hebben: Definition Hetero (x:M) := ∃ y:M, ( isMan(x) ∧ isVrouw(y) ∧ Houdtvan(x,y) ) ∨ (isMan(y) ∧ isVrouw(x) ∧ Houdtvan(x,y) ) Mijn vraag is: Moet men voorkomen, dat x en y de gelijke persoon zijn en als ja hoe? Om het duidelijk te maken: Zou men uit deze definitie ook kunnen lezen, dat een man bv. van een vrouw houd en toevallig zijn man en vrouw dezelfde persoon? |
 |
|
| Patrick Schileffski → Beweren en bewijzen | Remove this comment when resolved! | |
| Op je vraag mag iemand anders ingaan. Ik plaats al een vraagteken bij "HoudtVan". Dit wordt hier op deze pagina's gemakkelijk gebruikt, en kennelijk weten jullie hoe men dit door "observeren/vragen" kan meten. Het gaat hierbij wel (in sommige landen) om leven en dood of (in somige kerken) om het eeuwige leven. Het toepassen van logica blijft geen onschuldig spelletje als men zich aan dit soort dingen waagt en er zo mee omgaat. (Zie ook een aantal recente artikelen op http://nl.rationalitas.eu .) |  |
|
| Hanno Wupper → Beweren en bewijzen | Remove this comment when resolved! | |
