Computational Semantics

2y ago
31 Views
2 Downloads
784.85 KB
228 Pages
Last View : 1d ago
Last Download : 3m ago
Upload by : Pierre Damon
Transcription

Computational SemanticsPhilippe de Groote2018-2019Philippe de GrooteComputational Semantics2018-20191 / 98

Outline I1Introduction2Mathematical preliminaries3Model-theoretic semantics4First-order logic5Syntax-semantics interface6λ-CalculusPhilippe de GrooteComputational Semantics2018-20192 / 98

Outline II7Syntax-semantics interface revisited8Noun phrases and quantified noun phrases9Noun and determiners10Relative clauses11Adjectives12Scope ambiguities13De re and de dicto readingsPhilippe de GrooteComputational Semantics2018-20193 / 98

Outline III14IntensionalityPhilippe de GrooteComputational Semantics2018-20194 / 98

IntroductionOutline1IntroductionPhilippe de GrooteComputational Semantics2018-20195 / 98

IntroductionIntoductionSemantics is the study of meaning.EntailmentEric is the husband of Rebecca and the father of John. Eric is the father of John. Eric is the husband of Rebecca.Formal semantics:The meaning of an utterance depends upon its form, i.e., its linguisticstructure.The tools used to account for the meanings of utterances are formalmathematical tool.Truth conditional semantics.Model theoretic semantics.Philippe de GrooteComputational Semantics2018-20196 / 98

Mathematical preliminariesOutline2Mathematical preliminariesNaive set theoryRelationFunctionsIdentitiesPhilippe de GrooteComputational Semantics2018-20197 / 98

Mathematical preliminariesNaive set theoryNaive set theoryMembershipx Ax is an element (or a member) of the set A.x belongs to A.x 6 Ax does not belong to A.InclusionA Bthe set A is a subset of the set B.every element x that belongs to A belongs to B.Philippe de GrooteComputational Semantics2018-20198 / 98

Mathematical preliminariesNaive set theoryNaive set theoryDefinition by extension{a, b, c}the set whose elements are a, b, and c.Definition by comprehension{x A : P }the set whose elements are the elements of A that obey the property P .example: {n N : n 0 and n 4} {1, 2, 3, 4}Philippe de GrooteComputational Semantics2018-20199 / 98

Mathematical preliminariesNaive set theoryNaive set theoryPowersetP(A)the set whose elements are the subsets of A.example:P({a, b, c}) {{}, {a}, {b}, {c}, {a, b}, {a, c}, {b, c}, {a, b, c}}Philippe de GrooteComputational Semantics2018-201910 / 98

Mathematical preliminariesNaive set theoryNaive set theoryIntersectionA Bthe set whose elements belongs to both A and B.example: {a, b, c} {b, c, d} {b, c}UnionA Bthe set whose elements belongs to A or B (or both).example: {a, b, c} {b, c, d} {a, b, c, d}DifferenceA\Bthe set whose elements belongs to both A but does not belong to B.example: {a, b, c} \ {b, c, d} {a}Philippe de GrooteComputational Semantics2018-201911 / 98

Mathematical preliminariesNaive set theoryNaive set theoryOrdered pair(a, b)the ordered pair whose first component (coordinate) is a and secondcomponent is b.Cartesian productA Bthe set of all the ordered pairs (a, b) such that a A and b B.A B Cthe set of all the 3-tuples (a, b, c) such that a A, and b B, andc C.A B C D .Philippe de GrooteComputational Semantics2018-201912 / 98

Mathematical preliminariesNaive set theoryNaive set theoryEmpty set the set that does not have any member.for every element x, x 6 .Natural numbers0 1 {0} { }2 {0, 1} { , { }}n {0, 1, . . . , n 1}Disjoint UnionA BA B ({0} A) ({1} B)Philippe de GrooteComputational Semantics2018-201913 / 98

Mathematical preliminariesRelationRelationsBinary relationR P(A B)A binary relation R between A and B is a subset of the cartesianproduct A B.In case (a, b) R, one says that a is related to b by R, and one writesa R b or R(a, b).n-ary relationR P(A1 A2 . . . An )In case (a1 , a2 , . . . , an ) R, one writes R(a1 , a2 , . . . , an ).Philippe de GrooteComputational Semantics2018-201914 / 98

Mathematical preliminariesFunctionsFunctionsFunctionA function f from A to B is a binary between A and B such that:- for every a A, there is a b B such that (a, b) f (totality);- for every a A and every b, c B, if (a, b) f and (a, c) f thenb c (functionality).In case (a, b) f , one says that f maps a to b, and one writesf (a) b.Set of functionsBAis the set of functions from A to B.Philippe de GrooteComputational Semantics2018-201915 / 98

Mathematical preliminariesFunctionsFunctionsCharacteristic functionLet B A. The characteristic function κB 2A is defined as follows:κB (a) 1 iff a BLet f 2A . The fiber f 1 (1) is the set defined as follows::f 1 (1) {a A : f (a) 1}Let B A. κ 1B (1) B and κf .Let f 2A . κf 1 (1) f .P(A) and 2A are isomorphic.Philippe de GrooteComputational Semantics2018-201916 / 98

Mathematical preliminariesIdentitiesIdentitiesThe set-theoretic notations (product, sum, exponential, natural numbers)are such that high-school algebraic identities hold between sets (up toisomorphism).Examples:A A ' A2A0 ' 1A1 ' AAB AC ' AB C.Philippe de GrooteComputational Semantics2018-201917 / 98

Model-theoretic semanticsOutline3Model-theoretic semanticsModelObject languageInterpretationPhilippe de GrooteComputational Semantics2018-201918 / 98

Model-theoretic semanticsModelModelInformal definitionA model is an abstract mathematical structure made of a set of entities(the interpretation domain), together with operations (i.e. functions) andrelations on that set.ExampleD {e, j, r}.F, H D2 .F {(e, j)}.H {(e, r)}.Philippe de GrooteComputational Semantics2018-201919 / 98

Model-theoretic semanticsObject languageObject languageDefinitionA first-order langage consists in two sets of symbols:A set F , together with an arity function arF NF , whose elementsare called function symbols.A set R, together with an arity function arR NR , whose elementsare called relation symbols.ExampleF {e, j, r, father};arF (e) 0, arF (j) 0, arF (r) 0, arF (father) 1;R {Is, Husband};arR (e) 2, arR (j) 2.Philippe de GrooteComputational Semantics2018-201920 / 98

Model-theoretic semanticsObject languageObject languageTermsLet X be a countably infinite set of symbols whose elements are calledvariables. The set of terms is inductively defined as follows:every x X is a term;every a F such that arF (a) 0 is a term,if f F with arF (f ) n and n 0, and if t1 , . . . , tn are terms,then f (t1 , . . . , tn ) is a term.Propositionif R R with arR (R) n, and if t1 , . . . , tn are terms, thenR(t1 , . . . , tn ) is an atomic proposition.ExampleTerms: e; father(j); father(father(r)); father(x).Proposition: Is(e, father(j)); Husband(e, r).Philippe de GrooteComputational Semantics2018-201921 / 98

Model-theoretic semanticsInterpretationInterpretationModelGiven a first-order langage, a model consists of a set D and aninterpretation function I defined on F R such that:nfor every f F with arF (f ) n, I(f ) DD ;nfor every R R with arR (R) n, I(R) 2D .ExampleD NI(e) 6I(j) 3I(r) 7I(father) f NN such that f (n) 2nI(Is) {(a, b) N2 : a b}I(Husband) {(a, b) N2 : a 2n and b a 1 for some n N}Philippe de GrooteComputational Semantics2018-201922 / 98

Model-theoretic n of the ground termsGiven a first-order langage, and a model, the interpretation of the groundterms is inductively defined as follows:JaK I(a), for a F with arF (a) 0;Jf (t1 , . . . , tn )K I(f )(Jt1 K, . . . , Jtn K), for f F with arF (f ) nand n 0.ExampleJfather(father(r))K I(father)(Jfather(r)K) 2 · (Jfather(r)K) 2 · (I(father)(JrK)) 2 · (2 · JrK) 2 · (2 · 7) 28Philippe de GrooteComputational Semantics2018-201923 / 98

Model-theoretic n of the closed atomic propositionsGiven a first-order langage, and a model, the interpretation of the closedatomic propositions is defined as follows:JR(t1 , . . . , tn )K I(R)(Jt1 K, . . . , Jtn K), for R R with arR (R) n.ExampleJIs(e, father(j))K I(Is)(JeK, Jfather(j)K) I(Is)(JeK, I(father)(JjK)) I(Is)(6, 2 · 3) I(Is)(6, 6) 1Philippe de GrooteComputational Semantics2018-201924 / 98

Model-theoretic n a first-order langage, and a model, a valuation is a a functionξ DX .Interpretation of the termsGiven a first-order langage, and a model, the interpretation of the terms isinductively defined as follows:JxKξ ξ(x), for x X ;JaKξ I(a), for a F with arF (a) 0;Jf (t1 , . . . , tn )Kξ I(f )(Jt1 Kξ , . . . , Jtn Kξ ), for f F with arF (f ) nand n 0.Philippe de GrooteComputational Semantics2018-201925 / 98

Model-theoretic n of the atomic propositionsGiven a first-order langage, and a model, the interpretation of the closedatomic propositions is defined as follows:JR(t1 , . . . , tn )Kξ I(R)(Jt1 Kξ , . . . , Jtn Kξ ), for R R witharR (R) n.Philippe de GrooteComputational Semantics2018-201926 / 98

First-order logicOutline4First-order logicPropositional logicQuantificationInterpretationPhilippe de GrooteComputational Semantics2018-201927 / 98

First-order logicPropositional logicPropositional logicpropositionsGiven a first-order language, the set of proposition is inductively defined asfollows:every atomic proposition is a proposition;if α is a proposition then α is a proposition;if α and β are propositions then (α β) is a proposition;if α and β are propositions then (α β) is a proposition;if α and β are propositions then (α β) is a proposition.ExamplePhilippe de GrooteHusband(e, r) Is(e, father(j))Computational Semantics2018-201928 / 98

First-order logicPropositional logicPropositional logicNegation αnot α.J αKξ 1 iff JαKξ 0.α α0 11 0Philippe de GrooteComputational Semantics2018-201929 / 98

First-order logicPropositional logicPropositional logicConjunctionα βα and β.Jα βKξ 1 iff JαKξ 1 and JβKξ 1.α0011Philippe de Grooteβ α β00100011Computational Semantics2018-201930 / 98

First-order logicPropositional logicPropositional logicDisjunctionα βα or β.Jα βKξ 1 iff JαKξ 1 or JβKξ 1 (or both).α0011Philippe de Grooteβ α β00110111Computational Semantics2018-201931 / 98

First-order logicPropositional logicPropositional logicImplicationα βIf α then β; α implies β.Jα βKξ 1 iff JβKξ 1 whenever JαKξ 1.α0011Philippe de Grooteβ α β01110011Computational Semantics2018-201932 / 98

First-order logicQuantificationQuantificationfirst-order formulasGiven a first-order language, the set of first-order formulas is inductivelydefined as follows:every atomic proposition is a first-order formula;if α is a first-order formula then α is a first-order formula;if α and β are first-order formulas then (α β) is a first-order formula;if α and β are first-order formulas then (α β) is a first-order formula;if α and β are first-order formulas then (α β) is a first-orderformula;if α is a first-order formulas and x a variable then ( x. α) is afirst-order formula;if α is a first-order formulas and x a variable then ( x. α) is afirst-order formula.ExamplePhilippe de Groote x. y. Is(y, father(x))Computational Semantics2018-201933 / 98

First-order logicQuantificationQuantificationUniversal quantification x. αevery entity x is such that α.J x. αKξ 1 iff JαKξ[x: d] 1 for every d D.Philippe de GrooteComputational Semantics2018-201934 / 98

First-order logicQuantificationQuantificationExistential quantification x. αThere is some entity x such that α.J x. αKξ 1 iff JαKξ[x: d] 1 for some d D.Philippe de GrooteComputational Semantics2018-201935 / 98

First-order logicInterpretationInterpretationLet a first-order language be given, and let φ, M , and ξ be respectively afirst-order formula, a model, and a valuation.M , ξ φM and ξ satisfy φ.φ is valid in M according to ξ.JφKξ 1.M φM satisfies φ.φ is valid in M .M , ξ φ for every possible valuation ξ. φφ is valid.M φ for every possible model M .Philippe de GrooteComputational Semantics2018-201936 / 98

Syntax-semantics interfaceOutline5Syntax-semantics interfaceUsing an object languageCompositionalityPhilippe de GrooteComputational Semantics2018-201937 / 98

Syntax-semantics interfaceUsing an object languageUsing an object languagePhilippe de GrooteComputational Semantics2018-201938 / 98

Syntax-semantics interfaceUsing an object languageUsing an object languagenatural languagePhilippe de GrooteComputational Semantics2018-201938 / 98

Syntax-semantics interfaceUsing an object languageUsing an object languagenatural language object languagePhilippe de GrooteComputational Semantics2018-201938 / 98

Syntax-semantics interfaceUsing an object languageUsing an object languagenatural language object languageEric is tall and thinPhilippe de GrooteComputational Semantics2018-201938 / 98

Syntax-semantics interfaceUsing an object languageUsing an object languagenatural language object languageEric is tall and thinPhilippe de Groote tall(e) thin(e)Computational Semantics2018-201938 / 98

Syntax-semantics interfaceUsing an object languageUsing an object languagenatural language object languageEric is tall and thin tall(e) thin(e)Rebecca has a husbandPhilippe de GrooteComputational Semantics2018-201938 / 98

Syntax-semantics interfaceUsing an object languageUsing an object languagenatural language object languageEric is tall and thin tall(e) thin(e)Rebecca has a husbandPhilippe de Groote x. husband(x, r)Computational Semantics2018-201938 / 98

Syntax-semantics interfaceUsing an object languageUsing an object languagenatural language object languageEric is tall and thin tall(e) thin(e)Rebecca has a husband x. husband(x, r)Eric has a wifePhilippe de GrooteComputational Semantics2018-201938 / 98

Syntax-semantics interfaceUsing an object languageUsing an object languagenatural language object languageEric is tall and thin tall(e) thin(e)Rebecca has a husbandEric has a wifePhilippe de Groote x. husband(x, r) x. husband(e, x)Computational Semantics2018-201938 / 98

Syntax-semantics interfaceUsing an object languageUsing an object languagenatural language object languageEric is tall and thin tall(e) thin(e)Rebecca has a husbandEric has a wife x. husband(x, r) x. husband(e, x)Everybody has a fatherPhilippe de GrooteComputational Semantics2018-201938 / 98

Syntax-semantics interfaceUsing an object languageUsing an object languagenatural language object languageEric is tall and thin tall(e) thin(e)Rebecca has a husbandEric has a wife x. husband(x, r) x. husband(e, x)Everybody has a fatherPhilippe de Groote x. y. Is(y, father(x))Computational Semantics2018-201938 / 98

Syntax-semantics interfaceUsing an object languageUsing an object languagePhilippe de GrooteComputational Semantics2018-201939 / 98

Syntax-semantics interfaceUsing an object languageUsing an object languagenatural languagePhilippe de GrooteComputational Semantics2018-201939 / 98

Syntax-semantics interfaceUsing an object languageUsing an object languagenatural language syntactic structurePhilippe de GrooteComputational Semantics2018-201939 / 98

Syntax-semantics interfaceUsing an object languageUsing an object languagenatural language syntactic structure object languagePhilippe de GrooteComputational Semantics2018-201939 / 98

Syntax-semantics interfaceUsing an object languageUsing an object languagenatural language syntactic structure object language modelPhilippe de GrooteComputational Semantics2018-201939 / 98

Syntax-semantics interfaceUsing an object languageUsing an object languagenatural language syntactic structure object language modelEric is tall and thinPhilippe de GrooteComputational Semantics2018-201939 / 98

Syntax-semantics interfaceUsing an object languageUsing an object languagenatural language syntactic structure object language modelSNPEric is tall and thin EricVPVisAPAAandtallPhilippe de GrooteComputational Semanticsthin2018-201939 / 98

Syntax-semantics interfaceUsing an object languageUsing an object languagenatural language syntactic structure object language modelSNPEric is tall and thin EricVPVisAPA tall(e) thin(e)AandtallPhilippe de GrooteComputational Semanticsthin2018-201939 / 98

Syntax-semantics interfaceCompositionalityCompositionalityThe principle of compositionalityAlso known as Frege’s principle:The meaning of a complex expression is determined by itsstructure and the meanings of its constituents.Philippe de GrooteComputational Semantics2018-201940 / 98

Syntax-semantics interfaceCompositionalityCompositionalityPhilippe de GrooteComputational Semantics2018-201941 / 98

Syntax-semantics VAPisAAandtallPhilippe de GrooteComputational Semanticsthin2018-201941 / 98

Syntax-semantics interfaceCompositionalityCompositionalitySNPVPEric eVAPisAAandtallPhilippe de GrooteComputational Semanticsthin2018-201941 / 98

Syntax-semantics interfaceCompositionalityCompositionalitySNPVPEric eVAPisAAandtall tall(x)Philippe de GrooteComputational Semanticsthin2018-201941 / 98

Syntax-semantics interfaceCompositionalityCompositionalitySNPVPEric eVAPisAAandtall tall(x)Philippe de GrooteComputational Semanticsthin thin(x)2018-201941 / 98

Syntax-semantics interfaceCompositionalityCompositionalitySNP eVPEric eVAPisAAandtall tall(x)Philippe de GrooteComputational Semanticsthin thin(x)2018-201941 / 98

Syntax-semantics interfaceCompositionalityCompositionalitySNP eVPEric eVAPisA tall(x)Aandtall tall(x)Philippe de GrooteComputational Semanticsthin thin(x)2018-201941 / 98

Syntax-semantics interfaceCompositionalityCompositionalitySNP eVPEric eVAPisA tall(x)andtall tall(x)Philippe de GrooteComputational SemanticsA thin(x)thin thin(x)2018-201941 / 98

Syntax-semantics interfaceCompositionalityCompositionalitySNP eVPEric eAP tall(x) thin(x)VisA tall(x)andtall tall(x)Philippe de GrooteComputational SemanticsA thin(x)thin thin(x)2018-201941 / 98

Syntax-semantics interfaceCompositionalityCompositionalitySNP eVP tall(x) thin(x)Eric eAP tall(x) thin(x)VisA tall(x)andtall tall(x)Philippe de GrooteComputational SemanticsA thin(x)thin thin(x)2018-201941 / 98

Syntax-semantics interfaceCompositionalityCompositionalityS tall(e) thin(e)NP eVP tall(x) thin(x)Eric eAP tall(x) thin(x)VisA tall(x)andtall tall(x)Philippe de GrooteComputational SemanticsA thin(x)thin thin(x)2018-201941 / 98

Syntax-semantics interfaceCompositionalityCompositionalityLet “tall” be a function from terms to formulas such that:tall(t) tall(t)Similarly, let:thin(t) thin(t)Let “and” be a function such that:and(f )(g)(t) f (t) g(t)If we write (A B) for the set of functions B A then “and” is a functionbelonging to the following set:(T F ) ((T F ) (T F ))where T and F are respectively the set of terms and the set of formulasof the object language.Philippe de GrooteComputational Semantics2018-201942 / 98

Syntax-semantics interfaceCompositionalityCompositionalityGrammar:S NP VPVP V APAP A and AA tallA thinNP EricSemantic rules:JSK JVPK (JNPK)JVPK JAPKJAP and (JA1 K) (JA2 K)JAK tallJAK thinJNPK ePhilippe de GrooteComputational Semantics2018-201943 / 98

Syntax-semantics interfaceCompositionalityCompositionalityPhilippe de GrooteComputational Semantics2018-201944 / 98

Syntax-semantics VAPisAAandtallPhilippe de GrooteComputational Semanticsthin2018-201944 / 98

Syntax-semantics interfaceCompositionalityCompositionalitySNP eVPEricVAPisAAandtallPhilippe de GrooteComputational Semanticsthin2018-201944 / 98

Syntax-semantics interfaceCompositionalityCompositionalitySNP eVPEricVAPisA tallAandtallPhilippe de GrooteComputational Semanticsthin2018-201944 / 98

Syntax-semantics interfaceCompositionalityCompositionalitySNP eVPEricVAPisA tallandtallPhilippe de GrooteComputational SemanticsA thinthin2018-201944 / 98

Syntax-semantics interfaceCompositionalityCompositionalitySNP eVPEricVAP and (tall) (thin)isA tallandtallPhilippe de GrooteComputational SemanticsA thinthin2018-201944 / 98

Syntax-semantics interfaceCompositionalityCompositionalitySNP eVP and (tall) (thin)EricVAP and (tall) (thin)isA tallandtallPhilippe de GrooteComputational SemanticsA thinthin2018-201944 / 98

Syntax-semantics interfaceCompositionalityCompositionalityS tall(e) thin(e)NP eVP and (tall) (thin)EricVAP and (tall) (thin)isA tallandtallPhilippe de GrooteComputational SemanticsA thinthin2018-201944 / 98

sβ-ReductionSimple typesinterpretationLogical constantsPhilippe de GrooteComputational Semantics2018-201945 / 98

λ-Calculusλ-Notatationλ-Notatation“2x y”Philippe de GrooteComputational Semantics2018-201946 / 98

λ-Calculusλ-Notatationλ-Notatation“2x y”f (x) 2x yPhilippe de GrooteComputational Semantics2018-201946 / 98

λ-Calculusλ-Notatationλ-Notatation“2x y”f (x) 2x yλx. 2x yPhilippe de GrooteComputational Semantics2018-201946 / 98

λ-Calculusλ-Notatationλ-Notatation“2x y”f (x) 2x yλx. 2x yf (y) 2x yPhilippe de GrooteComputational Semantics2018-201946 / 98

λ-Calculusλ-Notatationλ-Notatation“2x y”f (x) 2x yλx. 2x yf (y) 2x yλy. 2x yPhilippe de GrooteComputational Semantics2018-201946 / 98

λ-Calculusλ-Notatationλ-Notatation“2x y”f (x) 2x yλx. 2x yf (y) 2x yλy. 2x yf (x, y) 2x yPhilippe de GrooteComputational Semantics2018-201946 / 98

λ-Calculusλ-Notatationλ-Notatation“2x y”f (x) 2x yλx. 2x yf (y) 2x yλy. 2x yf (x, y) 2x yλxy. 2x yPhilippe de GrooteComputational Semantics2018-201946 / 98

λ-Calculusλ-Termsλ-TermsLet C be a set of symbols whose elements are called constants, and let Xbe a countably infinite set of symbols, disjoint from C , whose elements arecalled λ-variables. The set of λ-terms is inductively defined as follows:every c C is a λ-term;every x X is a λ-term;if t is a λ-term and x is a λ-variable then (λx. t) is a λ-term;if t and u are λ-terms then (t u) is a λ-term.Philippe de GrooteComputational Semantics2018-201947 / 98

λ-Calculusλ-Termsλ-TermsAbstraction(λx. t)Philippe de GrooteComputational Semantics2018-201948 / 98

λ-Calculusλ-Termsλ-TermsAbstraction(λx. t)The function that maps x to t.t is called the body of the abstraction.The free occurences of x in t are bound in (λx. t).Philippe de GrooteComputational Semantics2018-201948 / 98

λ-Calculusλ-Termsλ-TermsAbstraction(λx. t)The function that maps x to t.t is called the body of the abstraction.The free occurences of x in t are bound in (λx. t).CurryficationPhilippe de GrooteComputational Semantics2018-201948 / 98

λ-Calculusλ-Termsλ-TermsAbstraction(λx. t)The function that maps x to t.t is called the body of the abstraction.The free occurences of x in t are bound in (λx. t).Curryficationg(x, y) x yPhilippe de GrooteComputational Semantics2018-201948 / 98

λ-Calculusλ-Termsλ-TermsAbstraction(λx. t)The function that maps x to t.t is called the body of the abstraction.The free occurences of x in t are bound in (λx. t).Curryficationg(x, y) x yfx (y) x yg 0 (x) fxPhilippe de GrooteComputational Semantics2018-201948 / 98

λ-Calculusλ-Termsλ-TermsAbstraction(λx. t)The function that maps x to t.t is called the body of the abstraction.The free occurences of x in t are bound in (λx. t).Curryficationg(x, y) x yfx (y) x yg 0 (x) fxPhilippe de Grooteg 0 (x)(y) fx (y) x y g(x, y)Computational Semantics2018-201948 / 98

λ-Calculusλ-Termsλ-TermsApplication(t u)Philippe de GrooteComputational Semantics2018-201949 / 98

λ-Calculusλ-Termsλ-TermsApplication(t u)The function t applied to the argument u.t is called the operator, and u the operand.Philippe de GrooteComputational Semantics2018-201949 / 98

λ-Calculusλ-Termsλ-TermsApplication(t u)The function t applied to the argument u.t is called the operator, and u the operand.Usual notations:f : x 7 x 1f (3)Philippe de GrooteComputational Semantics2018-201949 / 98

λ-Calculusλ-Termsλ-TermsApplication(t u)The function t applied to the argument u.t is called the operator, and u the operand.Usual notations:f : x 7 x 1f (3)λ-calculus notations:λx. add x 1(λx. add x 1) 3Philippe de GrooteComputational Semantics2018-201949 / 98

λ-Calculusβ-Reductionβ-ReductionSubstitutionLet t and u be λ-terms, and x be a λ-variable. t[x : u] denotes theλ-term obtained by substituting u for the free occurrences of x in t. It isinductively defined as follows:t[c : u] c, for c C .x[y : u] y, for y X , and y 6 x.x[x : u] u(λy. t0 )[x : u] (λy. t0 [x : u]), where y 6 x and y not free in u.(t0 t1 )[x : u] (t0 [x : u] t1 [x : u])Philippe de GrooteComputational Semantics2018-201950 / 98

λ-Calculusβ-Reductionβ-ReductionNotion of β-reduction(λx. t) u β t[x : u]Relation of β-contractionC[(λx. t) u] β C[t[c : u]]Relation of β-reductionThe reflexive, transitive closure of the relation of β-contraction.t β uRelation of β-equivalenceThe reflexive, transitive, symmetric closure of the relation ofβ-contraction.t β uPhilippe de GrooteComputational Semantics2018-201951 / 98

λ-Calculusβ-Reductionβ-ReductionChurch-Rosser propertyLet t0 , t1 , and t2 be λ-terms such thatt0 β t1t0 β t2Then, there exists a λ-term t3 such thatt1 β t3t2 β t3Philippe de GrooteComputational Semantics2018-201952 / 98

λ-Calculusβ-Reductionβ-ReductionChurch-Rosser propertyLet t0 , t1 , and t2 be λ-terms such thatt0 β t1t0 β t2Then, there exists a λ-term t3 such thatt1 β t3t2 β t3Corollary: unicity of the normal forms.Philippe de GrooteComputational Semantics2018-201952 / 98

λ-Calculusβ-Reductionβ-ReductionExercice:Reduce the following terms:1(λx. y x x) z2(λxy. y x x) y3(λf x. f (f x) (λy. y) x) (λyz. z)4(λx. x x) (λy. y)5(λx. x x) (λx. x x)Philippe de GrooteComputational Semantics2018-201953 / 98

λ-CalculusSimple typesSimple typesDefinitionLet A be a set of symbols whose elements are called atomic types The setof simple types is inductively defined as follows:every a A is a simple type;if α and β are simple types then (α β) is a simple type.Philippe de GrooteComputational Semantics2018-201954 / 98

λ-CalculusSimple typesSimple typesDefinitionLet A be a set of symbols whose elements are called atomic types The setof simple types is inductively defined as follows:every a A is a simple type;if α and β are simple types then (α β) is a simple type.Philippe de GrooteComputational Semantics2018-201954 / 98

λ-CalculusSimple typesSimple typesDefinitionLet A be a set of symbols whose elements are called atomic types The setof simple types is inductively defined as follows:every a A is a simple type;if α and β are simple types then (α β) is a simple type.The intended meaning is that (α β) is the type of the λ-terms thatstand for functions whose domain is α, and range β.Philippe de GrooteComputational Semantics2018-201954 / 98

λ-CalculusSimple typesSimple typesDefinitionLet A be a set of symbols whose elements are called atomic types The setof simple types is inductively defined as follows:every a A is a simple type;if α and β are simple types then (α β) is a simple type.The intended meaning is that (α β) is the type of the λ-terms thatstand for functions whose domain is α, and range β.Given a set of atomic type A , we write T (A ) for the set of simple typesbuilt upon A .Philippe de GrooteComputational Semantics2018-201954 / 98

λ-CalculusSimple typesSimple typesSignatureA higher-order signature is a triple Σ (A , C , τ ), where:A is a set of atomic types;C is a set of constants;τ T (A )C is a function that assigns each constant in C with asimple type built on A .Philippe de GrooteComputational Semantics2018-201955 / 98

λ-CalculusSimple typesSimple typesSignatureA higher-order signature is a triple Σ (A , C , τ ), where:A is a set of atomic types;C is a set of constants;τ T (A )C is a function that assigns each constant in C with asimple type built on A .Philippe de GrooteComputational Semantics2018-201955 / 98

λ-CalculusSimple typesSimple typesTyping environmentGiven a signature a typing environment Γ is a finite set of ordered pairs(x, α) X T (A ) such that (x, α), (x, β) Γ implies α β.Given a typing environment Γ such that for every (y, β) Gamma y 6 x,we write “Γ, x:α” for the typing environment “Γ {(x, α)}”.Philippe de GrooteComputational Semantics2018-201956 / 98

λ-CalculusSimple typesSimple typesTyping environmentGiven a signature a typing environment Γ is a finite set of ordered pairs(x, α) X T (A ) such that (x, α), (x, β) Γ implies α β.Given a typing environment Γ such that for every (y, β) Gamma y 6 x,we write “Γ, x:α” for the typing environment “Γ {(x, α)}”.Typing judgementA typing judgement is an expression of the formΓ t:αwhere Γ is a typing environment, t a λ-term, and α a simple type.Philippe de GrooteComputational Semantics2018-201956 / 98

λ-CalculusSimple typesSimple typesTyping rulesΓ c : τ (c)Γ, x : α x : αΓ, x : α t : βΓ (λx. t) : (α β)Γ t : (α β)Γ u:αΓ (t u) : βPhilippe de GrooteComputational Semantics2018-201957 / 98

λ-CalculusSimple typesSimple typesTypable termsA λ-term t is typable if and only if there exist a typing environment Γ anda simple type α such thatΓ t:αPhilippe de GrooteComputational Semantics2018-201958 / 98

λ-CalculusSimple typesSimple typesTypable termsA λ-term t is typable if and only if there exist a typing environment Γ anda simple type α such thatΓ t:αNormalizationEvery typable term has a normal form.Philippe de GrooteComputational Semantics2018-201958 / 98 page

Formal semantics: The meaning of an utterance depends upon its form, i.e., its linguistic structure. The tools used to account for the meanings of utterances are formal mathematical tool. Truth conditional semantics. Model theoretic semantics. Ph

Related Documents:

Computational semantics is an interdisciplinary area combining insights from formal semantics, computational linguistics, knowledge representation and automated reasoning. The main goal of computational semantics is to find techniques for automatically con-structing semantic representation

What is computational semantics? Why use functional programming for computational semantics? Today, as a rst sample of computational semantics, we present a natural language engine for talking about classes. Material for this course is taken from Jan van Eijck and Christina Unger,Comp

Introduction 1 Introduction 2 Meaning 3 Types and Model Structure 4 Montague Semantics 5 Phenomena at the Syntax-Semantics Interface 6 Abstract Categorial Grammars 7 Underspeci cation 8 Discourse 9 Selected Bibliography Sylvain Pogodalla (LORIA/INRIA) Computational Semantics

Formal Specification [Best – E.g. Denotational Semantics– RD Tennent, Operational Semantics, Axiomatic Semantics] E.g. Scheme R5RS, R6RS Denotational Semantics Ada83 – “Towards a Formal Description of Ada”, Lecture Notes in Computer Science, 1980. C Denotational Semantics

computational semantics, and when a property should be deemed “true” computationally. Recently, Datta et al. in [13] gave a computational semantics to the syntax of their Protocol Composition Logic of [16,12] (cf. als

Computational Semantics form and content, or in terms of its status in learning and reasoning—without denying that key judgments require the synthesis of knowledge of both kinds. This perspective informs my

Computational Semantics Aljoscha Burchardt Stephan Walter Alexander Koller Michael Kohlhase Patrick Blackburn Johan Bos MiLCA, Saarbrücken. Abstract The most central fact about natural language is that it has meaning. Semantics is the study of meaning. In formal sema

ANSI A300 (Part 6)-2005 Transplanting, ANSI Z60.1- 2004 critical root zone: The minimum volume of roots necessary for maintenance of tree health and stability. ANSI A300 (Part 5)-2005 Management . development impacts: Site development and building construction related actions that damage trees directly, such as severing roots and branches or indirectly, such as soil compaction. ANSI A300 (Part .