% Linguistic side-effects in the typed CBN with shift/reset % % Chung-chieh Shan. Linguistic side effects % (hereafter, LSE). % % We assume cbn-xi-calc.elf is loaded first. We extend that % calculus with constants. % % To be able to extend the type families defined in cbn-xi-calc.elf % (so we can define types e and t, and constants for alice, etc) % we need the %thaw declaration, which requires the unsafe flag. % This is OK: we are not proving any meta-theorems here; we use % Twelf as the term evaluator and the type evaluator (typechecker). % Add more primitive types (in addition to the pre-defined int). %thaw pure. % open the pure family so we can extend it. % Constants. See the section on types below for the assignments of types % to these constants. const : type. %name const C. alice : const. bob : const. john : const. love : const. like : const. see : const. mother : const. father : const. present: const. ^ : const -> const -> const. %infix left 105 ^. % Quantification % At the present, it is very lame -- just to get things going. % We use the concrete syntax for variables. % That is, we assume that forall1 binds the constant named c1. forall1 : const. c1 : const. % Interrogatives % At the present, it is very lame -- just to get things going. % We use concrete syntax for variables. % That is, we assume that que1 binds the constant named q1 and % que2 binds the constant named q2. % que : (const -> const) -> const. que1 : const. q1 : const. que2 : const. q2 : const. ctype : type. %name ctype R. % types of constants. ce : ctype. ct : ctype. ~> : ctype -> ctype -> ctype. %infix right 105 ~>. cp : ctype -> pure. %prefix 150 cp. e = cp ce. % Convenient abbreviations. t = cp ct. % convenient abbreviations p_et = cp (ce ~> ct). p_ee = cp (ce ~> ce). p_eet = cp (ce ~> ce ~> ct). p_eee = cp (ce ~> ce ~> ce). e*t = e *> pr t. et = (pr e) => pr t. % A sample denotation, built from constants: love ^ alice ^ bob. % ^ is meant as a constructor of constants, corresponding to the % application in the target language, the language of denotations. % See the type assigned to ^ in the section about types below. % All constants are expressions and values c: const -> exp. %prefix 150 c. val-c : val (c _). % now we define ways to `concatentate' expressions that are meant % to evaluate to constants. % The following is a strict special form. capply! : exp -> exp -> exp. % We now make two functions, which use the capply! special form internally. % These are strict functions. Also, the first argument is evaluated % first (to be more precise, both are curried strict functions). % The latter differs from the former in the order of arguments % (and hence, in the order of their evaluation). % All binders in our calculus must be annotated with types. capply = [t1] [t2] [x] [y] (!l t1 [x] (!l t2 [y] (capply! x y))) @ x @ y. ylppac = [t1] [t2] [x] [y] (!l t1 [x] (!l t2 [y] (capply! y x))) @ x @ y. % Sorry, neither Twelf nor our calculus have polymorphism, so we have % to specialize slashes (applications of capply) to specific types /eet = capply p_eet e. %infix left 105 /eet. /et = capply p_et e. %infix left 105 /et. /ee = capply p_ee e. %infix left 105 /ee. /eee = capply p_eee e. %infix left 105 /eee. % We need the following definitions rather than flipping the % arguments of /et and /ee. These are the strict functions in % both arguments, and the first argument is evaluated first. \et = ylppac e p_et. %infix left 105 \et. \ee = ylppac e p_ee. %infix left 105 \ee. % \ee = [x] [y] y /ee x. %infix left 105 \ee. % Just a regular inverse application \ = [x] [y] y @ x. %infix left 104 \. % `Applications' of quantifiers qapply = [q] [t1] (!l t1 [x] (capply! (c q) x)). forall-i = qapply forall1 t. % The first sample expression... lex1 = c alice \et (c love /eet c bob). % we now extend the eval relation to account for constants. -: eval (Q < capply! (c C1) (c C2)) (Q < c (C1 ^ C2)). % that was it. Enought to run all the examples. %query 1 1 (eval* (? lex1)) R. % R = c (love ^ bob ^ alice). % another introductory example: difference between strict and % non-strict lambdas: %query 1 1 eval* (? ((l T [x] (c alice)) @ (xi CT [f] (c bob)))) (c alice). %query 1 1 eval* (? ((!l T [x] (c alice)) @ (xi CT [f] (c bob)))) (c bob). % Sec 5.1 of LSE % Eq (29): Alice loves everyone's mother everyone = xi (e =^ t) [f] forall-i @ (f < c c1). lse29 = ? (c alice \et (c love /eet (everyone \ee c mother))). %query 1 1 (eval* lse29) R. % R = c (forall1 ^ (love ^ (mother ^ c1) ^ alice)). % which corresponds to Eq (31) or LSE. % Sec 5.4 of LSE: traces and wh-questions. trace = [TA] [S] xi S [f] (l TA [g] f < g). % Eq 47: alice\(love/__) lse47 = ? (c alice \et (c love /eet (trace (pr e) S))). %query 1 1 (eval* lse47) R. % Eq 48: Bob, Alice loves lse48 = ? (c bob \ lse47). %query 1 1 (eval* lse48) (c (love ^ bob ^ alice)). % R = c (love ^ bob ^ alice). who = [T] xi (e =^ T) [f] (qapply que1 T) @ (f < c q1). who2 = [T] xi (e =^ T) [f] (qapply que2 T) @ (f < c q2). % LSE 51: Alice saw who? lse51 = ? (c alice \et (c see /eet who U)). %query 1 1 (eval* lse51) R. % R = c (que1 ^ (see ^ q1 ^ alice)). % % The following is the unit test, to check we get the desired answer %%query 1 1 (eval* (? (lse51 @ c bob))) (c (see ^ bob ^ alice)). %query 1 1 (eval* lse51) (c (que1 ^ (see ^ q1 ^ alice))). % LSE53: Who did alice see? % NB: the type of trace reflects the fact it takes an effectful % argument (that is, who). lse53 = ? ((who S1) \ ? (c alice \et (c see /eet (trace (e =^ t =v p_et) S2)))). %query 1 1 (eval* lse53) (c (que1 ^ (see ^ q1 ^ alice))). % LSE 56: Whose mother did Alice see? lse56 = (who U1 \ee c mother) \ ? (c alice \et (c see /eet (trace (e =^ t =v p_et) S2))). %query 1 1 eval* (? lse56) (c (que1 ^ (see ^ (mother ^ q1) ^ alice))). % input and output % Note that the output is a strict function! % We need to know the value we are outputting. input = trace. output = [UA] [UR] (!l UA [x] xi (UA =^ ((pr UA) => pr UR)) [f] ((f < x) @ x)). % A specialization of trace, so TA is a pure type e. he = trace (pr e). % John's mother saw him lio1 = ? (((output e t @ c john) \ee c mother) \et (c see /eet he S)). %query 1 1 eval* lio1 (c (see ^ john ^ (mother ^ john))). % Binding and quantification % LSE (35): Everyone's father loves their mother. lse36 = ? ((((output e t @ everyone) \ee c father) \et (c love /eet (he S \ee c mother)))). % R = c (forall1 ^ (love ^ (mother ^ c1) ^ (father ^ c1))). %query 1 1 eval* lse36 (c (forall1 ^ (love ^ (mother ^ c1) ^ (father ^ c1)))). % LSI 40: * Her father loves everyone's mother lse40 = ? (((he S \ee c father) \et (c love /eet ((output e t @ everyone) \ee c mother)))). % That actually succeeds and evaluates to a function % (the evaluation within lambda is suspended) % This is the same case as in LSE (27). %query 1 1 eval* lse40 R. % But applying this function does get stuck -- as is the case in LSE Eq (28) %query 0 1 eval* (? (lse40 @ c bob)) R. % lse40 cannot be typed, see below. % LSE Sec 5.6. Superiority. % Eq (62): Who __ saw who? lse62 = ? ((who2 p_et) \ (? ((trace (e =^ p_et =v p_eet) (e =^ p_et) \et (c see /eet who t))))). %query 1 1 eval* lse62 (c (que2 ^ (que1 ^ (see ^ q1 ^ q2)))). % Eq (63): * Who did who see __? % See the typing after lse62 below why who\[who\(see/__)] can't be typed. % LSE Sec 5.5: Binding in wh-questions. % Eq (57): Who_i __ saw his_i mother? lse58 = (output e t @ who t) \ ? (trace (e =^ et =v p_et) (e =^ et) \et (c see /eet (he S3 \ee c mother))). %query 1 1 eval* (? lse58) (c (que1 ^ (see ^ (mother ^ q1) ^ q1))). % Eq (59): *Who_i did his_i mother see __? lse59 = (output e t @ who t) \ (? ((he (e =^ ((pr e) => T3)) \ee c mother) \et (c see /eet trace (e =^ t =v t) S3))). % In the untyped calculus, this does evaluate to a question %query 1 1 eval* (? lse59) (c (que1 ^ (see ^ q1 ^ (mother ^ q1)))). % As we see below, when we try to type lse59 we get a type error. % ---------------------------------------- % Cataphora % LSE (43a): Whose present for him did every boy see? % LSE (43b): *Which boy does his mother like? % It seems `every boy' can be replaced with `everyone'. % Even with that replacement the example is too complex for the % present work (see the notes on the future work). Here, we analyze a % simpler phrase, also considered in LSE: % % LSE44a: Alice's present for him_i, every boy_i saw % (Alice \ (present / input)) \ [(output (every \ boy)) \ (see / __)] % Again, we simplify and replace `every boy' with everyone. % LSE44a, albeit simpler than LSE43a, is anything but trivial. The above % straightforward analysis (repeated below in the Twelf format) % lse44a = (c alice \ee (c present /eee he (e =^ U))) \ % (? ((output e t @ everyone) \et % (c see /eet trace (e =^ t =v t) S3))). % does not work: output is evaluated before trace and so % trace acts as input, consuming the individual produced by the output. % One ad-hoc solution is to replace trace with the following `relay', % which accepts the input, does the action of trace, and then repeats % the output for the benefit of the term brought in. The relay can be written % in pseudo-code as follows: % let x = input in % let t = trace in % reset (let y = output x in t) % Or, in Twelf syntax: % t_alice_present_him = (e =^ t =v (pr e) => (pr t)). % in-out-relay = input (pr e) (e =^ t_alice_present_him => (pr t)) \ % (!l e [x] xi (e =^ t) [f] % (l t_alice_present_him [r] % ? ((output e t @ x) \ % (!l e [y] f < r)))). % With this, we are able to evaluate the simplified version of LSE44a, % with `everyone' being replaced by a concrete individual, Bob. % lse44a1 = (c alice \ee (c present /eee he (e =^ t))) \ % (? ((output e (t_alice_present_him => pr t) @ c bob) \et % (c see /eet in-out-relay))). % %query 1 1 eval* (? lse44a1) (c (see ^ (present ^ bob ^ alice) ^ bob)). % % But this still does not work for LSE44a: we need `everyone' to take % the scope over the entire sentence (so the body of the quantifier % forall will be a constant rather than a lambda term, resulting from % trace or in-out-relay). % There are two approaches: emulate shift/reset with two levels or two % prompts, generalizing reset, ?, into reset2, of the form % reset2 E = (reset E) () % We show a different approach: `raising' everyone into a wider scope. % everyone2 = [T] xi (e =^ T => pr t) [f] l T [x] forall-i @ ((f < c c1) @ x). % % lse44a = (c alice \ee (c present /eee he (e =^ t))) \ % (? ((output e (t_alice_present_him => pr t) @ % everyone2 t_alice_present_him) % \et % (c see /eet in-out-relay))). % % %query 1 1 eval* (? lse44a) % (c (forall1 ^ (see ^ (present ^ c1 ^ alice) ^ c1))). % The previous ad hoc attempt suggests a more principled solution: a term % raise-scope such that (raise-scope E) causes E to scope % over the whole sentence rather than over the clause. The term % raise-scope isn't general: it assumes the clause to be a function % T1 -> T2 where T1 is either e or an effectful term with the base type % e. In short, raise-scope assumes the clause is a gapped clause with % the gap to be filled by an individual. The latter restriction can be % easily lifted. Getting rid of the first assumption requires % emulating multi-prompt delimited control operators. % The (inferred) type of the phrase ``Alice's present for him'': % (c alice \ee (c present /eee he (e =^ t))) t_alice_present_him = (e =^ t =v et). raise-scope = [T] [T1] [T2] (l T [r] xi (e =^ T1 => T2) [f] l T1 [x] (!l e [y] (f < y)) @ r @ x). t_outputet = (e =^ et =v t). lse44a1 = (c alice \ee (c present /eee he (e =^ t))) \ (? ((raise-scope t_outputet t_alice_present_him (pr et) @ (output e t @ c bob)) \et (c see /eet trace t_alice_present_him (e =^ t)))). %query 1 1 eval* (? lse44a1) (c (see ^ (present ^ bob ^ alice) ^ bob)). lse44a = (c alice \ee (c present /eee he (e =^ t))) \ (? ((raise-scope t_outputet t_alice_present_him (pr et) @ (output e t @ everyone)) \et (c see /eet trace t_alice_present_him (e =^ t)))). %query 1 1 eval* (? lse44a) (c (forall1 ^ (see ^ (present ^ c1 ^ alice) ^ c1))). % The dual examples of cataphora: unacceptable anaphora: % LSE (43b), simplified: * Who does his mother like? % This is the same as LSE59, and has been considered before. % LSE (44b) * Every boy his mother likes, or simplified: % * Everyone his mother likes % (note the exception: ``Everyone but John his mother likes'' seems to % be acceptable). lse44b = (output e t @ everyone) \ (? ((he S1 \ee c mother) \et (c see /eet trace T2 S2))). % This actually works in the untyped CBN: %query 1 1 eval* (? lse44b) R. % c (forall1 ^ (see ^ c1 ^ (mother ^ c1))). % But it cannot be typed because the type of 'he' implies it cannot take % an impure expression such as (output e t @ everyone). % Again, we need types to prevent over-generation. % ------ % Typing % Tell our subtyping relation that constant types are subtypes of themselves. -: subtype (pr (cp R)) (pr (cp R)). % We need to extend the teval1 relation to assign types % to all our constants. -: teval1 (c alice) (at pr e). -: teval1 (c bob) (at pr e). -: teval1 (c john) (at pr e). -: teval1 (c love) (at pr p_eet). -: teval1 (c like) (at pr p_eet). -: teval1 (c see) (at pr p_eet). -: teval1 (c mother) (at pr (cp (ce ~> ce))). -: teval1 (c father) (at pr (cp (ce ~> ce))). -: teval1 (c present) (at pr (cp (ce ~> ce ~> ce))). -: teval1 (c forall1) (at pr (cp (ct ~> ct))). -: teval1 (c c1) (at pr e). -: teval1 (c que1) (at pr (cp (ct ~> (ce ~> ct)))). -: teval1 (c q1) (at pr e). -: teval1 (c que2) (at pr (cp ((ce ~> ct) ~> (ce ~> ce ~> ct)))). -: teval1 (c q2) (at pr e). % ^ is indeed an application (cut) -: teval1 (c (C1 ^ C2)) (at pr (cp R2)) <- teval1 (c C1) (at pr (cp (R1 ~> R2))) <- teval1 (c C2) (at pr (cp R1)). -: teval1 (capply! (at pr (cp (RA ~> RR))) (at pr (cp RA))) (at pr (cp RR)). -: teval1 (capply! E1 E2) (capply! E1' E2) <- teval1 E1 E1'. -: teval1 (capply! (at pr T1) E2) (capply! (at pr T1) E2') <- teval1 E2 E2'. % ---------------- % Sample typing %query 1 1 teval (c (love ^ bob ^ alice)) R. % R = pr t. %query 1 1 teval (c (forall1 ^ (love ^ (mother ^ c1) ^ alice))) (pr t). %query 1 1 teval (capply! (c mother) (c bob)) R. %query 1 1 teval (c mother /ee c bob) R. %query 1 1 teval lex1 (pr t). %query 1 1 teval (everyone \ee c mother) R. % R = e =^ t =v t. %query 1 1 teval lse29 (pr t). %query 1 1 teval (trace (pr e) (e =^ e *> pr t)) R. %query 1 1 teval (c love /eet (trace (pr e) S)) R. % R = e *> (pr t) =^ U1 =v (pr e) => (pr U1); % S = e =^ U1. %query 1 1 teval (c alice \et (c love /eet (trace (pr e) S))) R. %query 1 1 teval (? (c alice \et (c love /eet (trace (pr e) S)))) R. %query 1 1 teval (? (c alice \et (c love /eet (trace (pr e) (e =^ t))))) (pr (pr e) => (pr t)). % The type of the trace is as behooves of a traced statement %query 1 1 teval lse47 R. % R = pr (pr e) => (pr t). %query 1 1 teval lse48 (pr t). % As behooves of a question... %query 1 1 teval lse51 R. % R = pr (pr e) => (pr t). %query 1 1 teval (who U) (e =^ t =v p_et). %query 1 1 teval (c alice \et (c see /eet trace (e =^ t =v p_et) S)) R. %query 1 1 teval (? (c alice \et (c see /eet trace (e =^ t =v p_et) S))) R. % R = pr (e =^ t =v p_et) => (pr p_et); % S = e =^ t. % As behooves of a question. %query 1 1 teval lse53 R. % R = pr p_et. %query 1 1 teval (who U \ee c mother) (e =^ t =v p_et). %query 1 1 teval lse56 (pr p_et). %query 1 1 teval ((!l e [x] xi S [f] ((f < x) @ x)) @ everyone) R. %query 1 1 teval (output e T @ everyone) (e =^ et =v t). %query 1 1 teval ((((output e t @ everyone) \ee c father) \et (c love /eet (he S \ee c mother)))) R. % R = t =^ t =v t; % S = e =^ t. %query 1 1 teval lse36 (pr t). %query 1 1 teval (((he S \ee c father) \et (c love /eet ((output e t @ everyone) \ee c mother)))) R. % R = t =^ et =v et; % This demonstrates why lse40 must be mis-typed: % ? (at R) cannot be of type t % because t cannot be of the type et. %query 0 1 teval lse40 R. %query 1 1 teval (? ((trace (e =^ p_et =v U2) (e =^ p_et) \et (c see /eet who t)))) R. % R = pr (e =^ p_et =v U2) => (pr U2); % That is, the inferred type is e~>e~>t %query 1 1 teval lse62 (pr p_eet). % Eq (63): * Who did who see __? % That won't type. In fact, even the subterm % who \et (see /eet trace) cannot be typed. %query 1 1 teval (c see /eet trace (pr e) (e =^ U)) (p_et =^ U =v (pr e) => (pr U)). %query 1 1 teval (who (cp B)) (e =^ cp B =v cp (ce ~> B)). %query 1 1 teval (who2 p_et) (e =^ p_et =v p_eet). % that is, who \et, partially applied %query 1 1 teval ((!l e [x] (!l p_et [y] (capply! y x))) @ (who B)) (p_et *> (pr t) =^ t =v cp (ce ~> ct)). %query 1 1 teval ((!l e [x] (!l p_et [y] (capply! y x))) @ (who2 p_et)) (p_et *> (pr t) =^ p_et =v cp (ce ~> ce ~> ct)). %query 1 1 teval (who t \et (at p_et =^ U1 =v t)) R. % R = t =^ U1 =v cp (ce ~> ct); % U1 = U1. %query 1 1 teval (who2 p_et \et (at p_et =^ U1 =v p_et)) R. % R = t =^ U1 =v cp (ce ~> ce ~> ct); % U1 = U1. % But (c see /eet trace (pr e) (e =^ U)) cannot fit the pattern % (at p_et =^ U1 =v cp B) above because the final answertype is % (pr e) => (pr U), which cannot be the base type cp B. %query 0 1 teval (who t \et (c see /eet trace (pr e) (e =^ U))) R. % Binding in wh-questions %query 1 1 teval (output e t @ who t) (e =^ (pr e) => (pr t) =v p_et). %query 1 1 teval (trace (e =^ et =v p_et) (e =^ et) \et (c see /eet (he (e =^ t) \ee c mother))) R. % R = t =^ t =v (e =^ et =v p_et) => (pr p_et). %query 1 1 teval ((output e t @ who t) \ (? (trace (e =^ et =v p_et) (e =^ et) \et (c see /eet (he S3 \ee c mother))))) (pr p_et). %query 1 1 teval lse58 (pr p_et). % LSE (59): * Who_i did his_i mother see __? % That will not type. % The reason: the raised phrase [his_i mother see __] %query 1 1 teval (? ((he (e =^ ((pr e) => T3)) \ee c mother) \et (c see /eet trace (e =^ t =v t) S3))) R. % has R = (pr e) => (pr e) => T3 % That is, the argument of the raised phrase must be a pure term, of type e. % But ``output who'' is definitely not a pure term. % Typing cataphora %query 1 1 teval (c alice \ee (c present /eee he (e =^ U))) R. % R = e =^ U =v (pr e) => (pr U); %query 1 1 teval (output e t @ c bob) (e =^ et =v t). %query 1 1 teval (raise-scope (e =^ et =v t) t_alice_present_him (pr et) @ (output e t @ c bob)) R. % R = e =^ t_alice_present_him => (pr et) =v % t_alice_present_him => (et =^ et =v t). %query 1 1 teval (c see /eet trace (e =^ U =v (pr e) => (pr U)) (e =^ U)) R. % R = p_et =^ U =v (e =^ U =v (pr e) => (pr U)) => (pr (pr e) => (pr U)) % Both cataphora sentences are well-typed and have the types of % propositions. %query 1 1 teval (? lse44a1) (pr t). %query 1 1 teval (? lse44a) (pr t).