msc_ a

Size: px
Start display at page:

Download "msc_ a"

Transcription

1 Math. Struct. in omp. Science (2018), vol. 28, pp c ambridge University Press 2017 doi: /s First published online 18 April 2017 oinductive predicates and final sequences in a fibration IHIRO HASUO, TOSHIKI KATAOKA, and KENTA HO Department of omputer Science, The University of Tokyo, Tokyo , Japan Research Fellow of Japan Society for the Promotion of Science, 5-3-1, Kouji-machi, hiyoda-ku, Tokyo , Japan Institute for omputing and Information Sciences, Radboud University, P.O.Box 9010, 6500 GL Nijmegen, the Netherlands Received 9 January 2015; revised 22 November 2016 oinductive predicates express persisting safety specifications of transition systems. Previous observations by Hermida and Jacobs identify coinductive predicates as suitable final coalgebras in a fibration a categorical abstraction of predicate logic. In this paper, we follow the spirit of a seminal work by Worrell and study final sequences in a fibration. Our main contribution is to identify some categorical size restriction axioms that guarantee stabilization of final sequences after ω steps. In its course, we develop a relevant categorical infrastructure that relates fibrations and locally presentable categories, a combination that does not seem to be studied a lot. The genericity of our fibrational framework can be exploited for binary relations (i.e. the logic of binary predicates ) for which a coinductive predicate is bisimilarity, constructive logics (where interests are growing in coinductive predicates) and logics for name-passing processes. 1. Introduction oinductive predicates postulate properties of state-based dynamic systems that persist after a succession of transitions. In computer science, safety properties of non-terminating, reactive systems are examples of paramount importance. This has led to an extensive study of specification languages in the form of fixed point logics and model-checking algorithms. In this paper, we follow Hermida and Jacobs (1998) and Hermida (1993) whose results are further extended in Fumex et al. (2011) and Atkey et al. (2012), see also Jacobs (2012, hap. 6) and take a categorical view on coinductive predicates. Here, coalgebras represent transition systems; a fibration is a predicate logic ; and a coinductive predicate is identified as a suitable coalgebra in a fibration. Our contribution is the study of final sequences an iterative construction of final coalgebras that is studied notably in Worrell (2005) and Adámek (2003) in such a fibrational setting. oalgebras have been successfully used as a categorical abstraction of transition systems (see e.g. Jacobs (2012); Rutten (2000)): By varying base categories and functors, coalgebras bring general results that work for a variety of systems at once. Fixed point logics (or modal logics in general), too, have been actively studied coalgebraically: oalgebraic

2 oinductive predicates and final sequences in a fibration 563 modal logic is a prolific research field (see îrstea et al. 2011); their base category is typically Sets but works like Klin (2007) go beyond and use presheaf categories for processes in name-passing calculi; and literature including îrstea and Sadrzadeh (2008), Venema (2006) and îrstea et al. (2009) studies coalgebraic fixed point logics. Unlike most of these works, we follow Hermida and Jacobs (1998) and Hermida (1993) and parameterize the underlying predicate logic too with the categorical notion of fibration. The conventional setting of classical logic is represented by the fibration Pred Sets (see Appendix for an introduction to fibrations). fibration P p Pred Sets Rel Sets coalgebra invariant bisimulation final coalgebra coinductive predicate bisimilarity However, there are various other logics modelled as fibrations, and hence the fibrational language provides a uniform treatment of these different settings. An example is binary relations (instead of unary predicates) that form a fibration Rel (see Appendix ). In this Sets case, coinductive predicates are bisimilarity relations (see the above table, and Example 7.2 later). Another example is predicates in constructive logics. They are modelled by the subobject fibration of a topos. In fact, coinductive predicates in constructive logics are an emerging research topic: oinduction is supported in the theorem prover oq (based on the constructive calculus of constructions), see e.g. Bertot and Komendantskaya (2008), and working in oq, some interesting differences between classically equivalent (co)inductive predicates have been studied, e.g. in Nakata et al. (2011). Yet another example is modal logics for processes in various name-passing calculi. They are best modelled by the subobject fibration of a suitable (pre)sheaf category like Sets I and Sets F (Fiore and Turi 2001; Fiore and Staton 2006; Miculan 2008; Stark 1996; Staton 2011) oinductive predicates and their construction, conventionally In order to illustrate our technical contributions (Section 3), we here present a special case, with classical logic and Kripke models. We first introduce syntax. Definition 1.1 (Rudimentary logic Rν). In this tiny fragment of the μ-calculus, fixed-point operators are limited to the greatest one at the outermost position; and moreover, all the formulas are rank-1, that is, the fixed-point variable u occurs precisely under one modal operator. Rν u α ::= a a u u α α α α ; Rν β ::= νu.α. (1) Here, a belongs to the set AP of atomic propositions; a stands for the negation of a and u is the only fixed-point variable (with possibly multiple occurrences).

3 I. Hasuo, T. Kataoka and K. ho 564 An Rν-formula can be thought of as a recursive definition of a coinductive predicate. Later, we will model such a definition categorically as a predicate lifting. Among specifications expressible in Rν is (may-) deadlock freedom (there is an infinite path). It is expressed by νu.u and is our recurring example. An Rν-formula is interpreted in Kripke models. Let c =(X,,V) be a Kripke model, where X is a state space, X X is a transition relation and V : X P(AP) isa valuation. The conventional interpretation [νu.α] c of Rν-formulas in the Kripke model c is given as follows (see e.g. Bradfield and Stirling (2006)). First, we interpret α Rν u as a function [α] c : PX PX. oncretely: [a] c (P )={x a V (x)} [a] c (P )={x a V (x)} [u] c (P )={x y X.(x y implies y P )} [α α ] c (P )=[α] c (P ) [α ] c (P ) [u] c (P )={x y X.(x y and y P )} [α α ] c (P )=[α] c (P ) [α ] c (P ) This function [α] c is easily seen to be monotone, since u occurs only positively in α. Finally, we define [νu.α] c X to be the greatest fixed point of the monotone function [α] c : PX PX. The Knaster Tarski theorem guarantees the existence of such a greatest fixed point [νu.α] c in a complete lattice PX. However, its proof is highly non-constructive. In contrast, a well-known iterative construction (ousot and ousot 1979) computes [νu.α] c as the limit of the following descending chain (see also Bradfield and Stirling (2006)). Here, denotes the subset X X. [α] c [α] 2 c. (2) An issue now is the length of the chain. If [α] c preserves limits (which is the case with α u), clearly ω steps are enough and yields i ω( [α] i c ) as the greatest fixed point. This is not the case with α u. Indeed, for the Kripke model c 1 below [νu.u] c1 i ω( [u] i c1 ) : there is no infinite path from the root; but it satisfies [u] i c 1 (there is a path of length i) foreachi. c 1 (3). Yet the chain (2) eventually stabilizes, bounded by the size of the poset PX: Ineachstep before stabilization, at least one element must be thrown away. Therefore, the calculation of [νu.α] c proceeds, in general, via transfinite induction. This is what we call a state space bound for the chain (2). Besides a state space bound, another (possibly better and seemingly less known) bound can be obtained from a behavioural view. One realizes that not only the size of the state space X but also the branching degree can be used to bound the length of the chain(2).

4 oinductive predicates and final sequences in a fibration 565 This is a result similar to the one in Hennessy and Milner (1985, Theorem 2.1); the latter is stated for bisimilarity as a coinductive relation, not for a coinductive predicate. We formally state (an instance of) the result for the record. Lemma 1.2 (Behavioural bound). Let c =(X,,V) be a finitely branching Kripke model. For α = u, the chain (2) stabilizes after ω steps and yields [νu.u] c as its limit, that is, i ω( [u] i c ) =[νu.u] c. Proof. The essence of the result lies in the fact that the limit i ω( [u] i c ) is a invariant, which we shall prove now. Assume that a state x satisfies i ω( [u] i c ) ( ;we have to show that x satisfies [u] c i ω( [u] i c )), that is, there is a successor x of x that satisfies the limit i ω( [u] i c ). Since x satisfies [u] i c (there is a path of length i) foreachi, foreachi 1, there is a successor x i of x that satisfies [u] c i 1. Byc being finitely branching, the set {x 1,x 2,...} of such successors turns out to be finite and there exists a successor x of x such that x = x i for infinitely many i. It follows (from [u] i c [u] j c if j i) that this x satisfies [u] i c for all i ω, and hence satisfies i ω( [u] i c ). This proves that the limit i ω( [u] i c ) is an invariant, and hence i ω( [u] i c ) [νu.u] c. For the last equality claimed in the lemma, the other direction [νu.u] c ( i ω [u] i c ) is easy: [νu.u] c [u] i c is easily shown by induction on i. This concludes the proof. Note that Lemma 1.2 holds however large the state space X is. Moreover, it easily generalizes from νu.u to an arbitrary Rν-formula νu.α. Note also that the counterexample c 1 in Equation (3) is not finitely branching and does not contradict with Lemma Final sequences in a fibration This paper is about putting the observations in Section 1.1 in general categorical terms. Our starting observation is that the chain (2) resembles a final sequence, a classic construction of a final coalgebra. In the theory of coalgebra, a final F-coalgebra is of prominent importance since it is a fully abstract domain with respect to the F-behavioural equivalence. Therefore, a natural question is if a final F-coalgebra exists; the well-known Lambek lemma prohibits e.g. a final P-coalgebra for the (full) powerset functor P. What matters is the size of F: When it is suitably bounded, it is known that a final coalgebra can be constructed via the following final F-sequence: 1! F1 F! F i 1! F i 1 F i!. (4) Here, 1 is a final object in, and! is the unique arrow. In particular, if F is finitary, a final coalgebra arises as a suitable subobject (or a quotient) of the ω-limit of the final sequence (4). These constructions in Sets are worked out in Pattinson (2003) and Worrell (2005); the one in Worrell (2005) is further extended to locally presentable categories (those are categories suited for speaking of size ) with additional assumptions in Adámek (2003).

5 I. Hasuo, T. Kataoka and K. ho 566 Turning back to coinductive predicates, indeed, the fibrational view (Hermida 1993; Hermida and Jacobs 1998) identifies coinductive predicates as final coalgebras in a fibration. This leads us to scrutinize final sequences in a fibration. Our main result (Theorem 3.9) is a categorical generalization of the behavioural ω-bound (Section 1.1) more precisely, we axiomatize categorical size restrictions for that bound to hold. The conditions are formulated in the language of locally presentable categories (see e.g. Adámek and Rosický (1994); also Appendix B); and the combination of fibrations and locally presentable categories does not seem to have been studied a lot (an exception is Makkai and Paré (1989, Section5.3)). We therefore develop a relevant categorical infrastructure (Section 6). Our results there include a sufficient condition for the total category Sub() of a subobject fibration to be locally (finitely) presentable, and the same for a family fibration Fam(Ω). Via these results, in Section 7, we list some concrete examples of fibrations to which our results in Section 3 on the behavioural bounds apply. They include Pred Rel Sub() (classical logic), Sets Sets (for bisimulation and bisimilarity), for that is locally finitely presentable (LFP) and locally artesian closed (a topos is a special case) Fam(Ω) and for a well-founded algebraic lattice Ω. Sets 1.3. ontributions To summarize, our contributions are (1) combination of the mathematical observations in Hermida (1993), Hermida and Jacobs (1998) and (Jacobs 2012, hap. 6) for a general formulation of coinductive predicates; (2) categorical behavioural bounds for final sequences that approximate coinductive predicates and (3) a categorical infrastructure that relates fibrations and locally presentable categories. ompared to the earlier version (Hasuo et al. 2013) of the current paper, the main differences are as follows. Here, we additionally address inductive predicates over coinductive datatypes (see Section 5). We identify them as coinductive predicates in the fibrewise P (op) opposite p (op) of the original fibration P p, so that the difference between inductive and coinductive predicates becomes a matter of categorical duality. The examples in Section 7 are extended accordingly, studying inductive predicates on top of coinductive ones. Besides, we include all the proofs that were omitted in Hasuo et al. (2013) for space reasons Organization of the paper In Section 2, we identify coinductive predicates as final coalgebras in a fibration, following the ideas of Hermida (1993), Hermida and Jacobs (1998) and Jacobs (2012). The main technical results are in Section 3, where we axiomatize size restrictions on fibrations and functors for a final sequence to stabilize after ω steps. These results are reorganized in Section 4 in a fibration of invariants. We see in Section 5, which is added to an earlier version of this paper (Hasuo et al. 2013), that the results in Section 2 4 apply to inductive

6 oinductive predicates and final sequences in a fibration 567 predicates too. The next two sections are devoted to examples: First in Section 6, we develop a necessary categorical infrastructure; and then in Section 7, we discuss concrete examples. In Section 8, we conclude with some directions of future work. In Appendices, we present minimal introductions to the theories of coalgebras, locally presentable categories and fibrations the three categorical disciplines that our technical developments rely on. 2. oinductive predicates as final coalgebras In this section, we follow the ideas in Hermida (1993), Hermida and Jacobs (1998), Jacobs (2012) and characterize coinductive predicates in various settings (for different behaviour types, and in various underlying logics) in the language of fibrations. An introduction to fibrations is e.g. in Jacobs (1999); see also Appendix. In this paper, for simplicity, we focus on poset fibrations. It should however not be hard to move to general fibrations. onvention 2.1 (Fibration). We refer to poset fibrations (where each fibre is a poset rather than a category) simply as fibrations. Definition 2.2 (Predicate lifting). Let P p be a fibration and F be an endofunctor on. A predicate lifting of F along p is a functor ϕ: P P such that (ϕ, F) is an endomap of fibrations. ϕ P P p p (5) F This means: that the above diagram commutes; and that ϕ preserves artesian arrows, that is, ϕ(f Q)=(Ff) (ϕq). See below. P p f Q fq Q ϕ(f Q) X f (Ff) (ϕq) Y FX Ff ϕ(fq) Ff(ϕQ) ϕq In the prototype example Pred, the above definition coincides (see Jacobs 2012) with Sets the one used in coalgebraic modal logic (see e.g. îrstea et al. (2011)), the latter being a (monotone) natural transformation 2 ( ) ϕ 2 F( ) : Sets op Sets. In particular, the naturality requirement corresponds to the preservation of artesian arrows (6); and monotonicity of ϕ comes from the functoriality of ϕ: P P. We think of predicate liftings as (co)recursive definitions of coinductive predicates (see Example 2.4). On top of it, we identify coinductive predicates (and invariants) as coalgebras in a fibre. FY (6)

7 I. Hasuo, T. Kataoka and K. ho 568 Definition 2.3 (Invariant, coinductive predicate). Let ϕ be a predicate lifting of F along P p ;andx c FX be a coalgebra in. They together induce an endofunctor (a monotone ϕ c function) on the fibre P X,namelyP X PFX P X,whereϕ restricts to P X P FX because of Equation (5). 1. A ϕ-invariant in c is a (c ϕ)-coalgebra in P X, that is, an object P P X such that P c (ϕp )inp X. 2. The ϕ-coinductive predicate in c is the final (c ϕ)-coalgebra (if it exists). Its carrier shall be denoted by νϕ c. It is therefore the largest ϕ-invariant in c; Lambek s lemma yields that νϕ c =(c ϕ)(νϕ c ). Example 2.4 (Rν). The conventional interpretation [νu.α] c (described in Section 1.1) of Rν-formulas is a special case of Definition 2.3. Indeed, let us work in the fibration Pred Sets, and with the endofunctor F K = P(AP) P( )onsets. AnF K -coalgebra X c P(AP) PX is precisely a Kripke model: c combines a valuation X P(AP) andthemapx PX that carries a state to the set of its successors. To each formula α Rν u,weassociatea predicate lifting ϕ α of F K. This is done inductively as follows: ϕ a (U X) = ( {V F K X a π 1 (V )} F K X ), ϕ a (U X) = ( {V F K X a π 1 (V )} F K X ), ϕ u (U X) = ( {V F K X π 2 (V ) U} F K X ), ϕ u (U X) = ( {V F K X π 2 (V ) U } F K X ), ϕ α α (U X) = ( (ϕ α U ϕ α U) F K X ), ϕ α α (U X) = ( (ϕ α U ϕ α U) F K X ). (7) In the above, π 1 and π 2 denote the projections from F K X = P(AP) PX. Then it is easily seen by induction that νϕ α c in Definition 2.3 coincides with the conventional interpretation [νu.α] c described in Section 1.1. In fact, the predicate liftings ϕ α in Equation (7) are the ones commonly used in coalgebraic modal logic (where they are presented as natural transformations). We point out that the same definition of ϕ α they are written in the internal language of toposes Sub() works for the subobject fibration of any topos. Therefore, the categorical definition of coinductive predicates (Definition 2.3) allows us to interpret the language Rν in constructive underlying logics. Suitable completeness of ensures that a final (c ϕ)-coalgebra in Definition 2.3 exists. Proposition 2.5. Let ϕ be a predicate lifting of F along P p ; X c FX be a coalgebra in ; andp P X. We have P νϕ c if and only if there exists a ϕ-invariant Q such that P Q. The proposition is trivial but potentially useful. It says that an invariant can be used as a witness for a coinductive predicate. This is how bisimilarity is commonly established

8 oinductive predicates and final sequences in a fibration 569 (namely by finding a bisimulation); and it can be used e.g. in Abramsky and Winschel (2015, Section 6) as an alternative to the metric coinduction principle used there. Remark 2.6. The coalgebraic modal logic literature exploits the fact that there can be many predicate liftings (in the form of natural transformations) of the same functor F. Different predicate liftings correspond to different modalities (such as vs. for the same functor P). This view of predicate liftings is also the current paper s concern (see Example 2.4). In contrast, in fibrational studies like Hermida (1993), Hermida and Jacobs (1998), Fumex et al. (2011) and Atkey et al. (2012), use of predicate liftings has focussed on the validity of the (co)induction proof principle. For such purposes, it is necessary to choose a predicate lifting ϕ that is comprehensive enough, covering all the possible F-behaviours. In fact, it is common in these studies that the predicate lifting, denoted by Pred(F), is assigned to a functor F. An exception is Jacobs (2010). 3. Final sequences in a fibration Here, we present our main technical result (Theorem 3.9). It generalizes known behavioural ω-bounds (like Hennessy and Milner (1985, Theorem 2.1); see Section 1.1); and claims that the chain (2) for a coinductive predicate stabilizes after ω steps, assuming that the behaviour type functor F and the underlying logic P p are finitary in a suitable sense (but no size restriction on ϕ) Size restrictions on a fibration We axiomatize finitariness conditions in the language of locally presentable categories (see Appendix B for a minimal introduction). Singling out these conditions lies at the heart of our technical contribution. Definition 3.1 (LFP category). Acategory is LFP if it is cocomplete and it has a (small) set F of finitely presentable (FP) objects such that every object is a filtered colimit of objects in F. Definition 3.2 (Finitely determined fibration). A (poset) fibration P p is finitely determined if it satisfies the following: 1. is LFP, with a set F of FP objects (as in Definition 3.1). 2. P p has fibrewise limits and colimits (as in Definition.9). 3. For arbitrary X, let(x I ) be the canonical diagram for X with respect to F κ I (i.e. I = F/X, see Lemma B.4), with a colimiting cocone (X I X). Then for any To be precise, only if we take PE in Abramsky and Winschel (2015) that is in fact, a least fixed-point specification as an atomic proposition (and that is essentially what is done in the proofs in Abramsky and Winschel (2015, Section 6)). Our future work on nested μ s and ν s will more adequately address the situation.

9 I. Hasuo, T. Kataoka and K. ho 570 P,Q P X, P Q κ IP κ IQ in P XI for each I I. The intuition behind ond. 3 is that a predicate P P X (over arbitrary X ) is determined by its restrictions (κ I P ) to FP objects X I. One convenient sufficient condition for ond. 3 is that the total category P is itself LFP, with its FP objects residing above the FP objects in (orollary 6.2). We note that ond. 1 guarantees, since LFP implies completeness, that an (ω op -)limit F ω 1 of the final F-sequence (4) exists. However, this does not mean (nor do we need) that F ω 1 carries a final F-coalgebra; it fails for F = P ω, see Worrell (2005). Definition 3.3 (Well-founded fibration). A well-founded fibration is a finitely determined fibration that further satisfies the following: 4. If X F (hence FP), the fibre P X is such that: the category P op X consists solely of FP objects. Since P X is complete, this is equivalent to: there is no (ω op -)chain P 0 >P 1 > in P X that is strictly descending. We note that the following stronger variant of the condition 3.3 rarely holds: 3.3 :Forany X, there is no strictly descending ω op -chain in P X (it fails in Pred ). The original ond. 3.3 holds in many examples (as we will see later Sets in Section 7), thanks to the restriction that X is FP. Remark 3.4. onditions mention a fixed set F of FP objects. It is not hard to see that this is not necessary, and we can take as F the set of all FP objects without loss of generality. (Stating the conditions in terms of F is an advantage when it comes to checking them, though.) Let us first note that, by Adámek and Rosický (1994, Remark 1.9), any FP object Y is a split quotient of some X F, i.e. there exists q : X Y and i: Y X with q i = id Y. Then we indeed have the following. On ond. 3, for an FP object Y and κ : Y X, take X F with a splitting X q i Y X.ThenwecantakeI such that X I = X and κ I = κ q. Hence, κ I P κ I Q in P X I induces κ P κ Q in P Y because κ = κ I i. On ond. 3.3, for an FP object Y,takeX F with a splitting X q Y i X. Then a strictly decreasing chain Q 0 >Q 1 > in P Y induces a strictly decreasing chain q Q 0 >q Q 1 > in P X. Here, the strictness of the latter is by i q Q n = Q n. The following trivial fact is written down for the record. Lemma 3.5. A finitely determined fibration P p is well-founded if P X is a finite category for each X F.

10 oinductive predicates and final sequences in a fibration 571 Fig. 1. Final sequences in a fibration. P ϕ ω 1 1 ϕ 1 ϕ i 1 ϕ ω+1 1 F ω 1 π i 1! F1 F i 1! F i F 1 i! Fπ i 1 F ω+1 1 b b 3.2. Final sequences in a fibration The following result from Jacobs (1999, Proposition 9.2.1) is crucial in our development. Lemma 3.6. Let P p be a fibration, with being complete. Then p has fibrewise limits if and only if P is complete and p: P preserves limits. If this is the case, a limit of a small diagram (P I ) in P can be given by (πi P I ) over Lim X I. π I Here, X I := pp I ;(Lim X I XI ) is a limiting cone in ; and denotes the the inf in the fibre P LimI X I.Moreover, (π I P I) is a limit of the diagram of shape I, namely πi P I πj P J holds for any I J in I. Figure 1 presents two sequences. Here, we assume that P p is finitely determined (Definition 3.2) and that ϕ is a predicate lifting of F. In the bottom diagram (in ), the object 1 is a final one (it exists since LFP implies completeness); F1! 1isthe unique map; F ω+1 1:=F(F ω 1); and b is a unique mediating arrow to the limit F ω 1. In the top diagram (in P), the object 1 is the final object in the fibre P 1 ; by Lemma 3.6, this is precisely a final object in the total category P. Hence, this diagram is nothing but a final sequence for the functor ϕ in P. A limit ϕ ω 1 of this final sequence exists, again by Lemma 3.6; and moreover, it can be chosen above F ω 1. We define ϕ ω+1 1 := ϕ(ϕ ω 1 ). Lemma 3.7 (Key lemma). Let P p be a well-founded fibration; F : be finitary; and ϕ be a predicate lifting of F. Then the final ϕ-sequence stabilizes after ω steps (modulo reindexing via b). Precisely, in Figure 1, we have ϕ ω+1 1 = b (ϕ ω 1 ). Proof. We proceed by steps. Step a. We observe that, in Figure 1, the top diagram is carried to the one below by the functor p: P. This is straightforward: The arrow ϕ 1 1 must be carried to the unique arrow!: F1 1; on the mediating arrow b in P, since pb is again a mediating arrow in, it must coincide with b.

11 I. Hasuo, T. Kataoka and K. ho 572 Step b. Before moving on, we observe that ond. 3 in Definition 3.2 yields a seemingly stronger statement (ond. 3 below). Sublemma 3.8. For a finitely determined fibration P p the following holds: 3 Let X ; P,Q P X ; and (Y J ) J J be an arbitrary filtered diagram in such that γ J olim J Y J = X, with a colimiting cocone (Y J X)J J. Then P Q if and only if for each J J, γj P γ J Q in P Y J. Proof. (Of Sublemma 3.8) The only non-trivial statement is the if part of the direction 3 3. It suffices to show that γj P γ J Q (for each J J) implies κ I P κ IQ (for each I I), where κ I and I are as in ond. 3. Let I I. Since X I is FP, an arrow κ I : X I X to a filtered colimit X = olim J Y J γ JI factors through some Y JI X, as in the diagram below. κ I X I X = olim J Y J h I Y JI γ JI Now, we have κ I P = h I γ J I P h I γ J I Q = κ IQ, where the inequality is by the assumption that γj P γ JQ for each J J. This proves Sublemma 3.8. Step c. By Step a, weseethatϕ ω+1 1 b (ϕ ω 1 ) by the universality of a artesian arrow. In what follows we shall prove its converse: b (ϕ ω 1 ) ϕ ω+1 1 in P F ω+1 1. (8) Let us take a filtered diagram (X I ) in such that X I F (for each I I) and F ω κ I 1=olim X I,with(X I F ω 1) being the colimiting cocone. Then we have F ω+1 1=F(olim X I )=olim FX I, Fκ I by the assumption that F is finitary; moreover, (FX I F ω+1 1) is a colimiting cocone. The diagram (X I ) is filtered, and so is the latter diagram (FX I ). Thus, by ond. 3 in Sublemma 3.8, showing the following proves Equation (8): (Fκ I ) ( b (ϕ ω 1 ) ) (Fκ I ) (ϕ ω+1 1 ) for each I I. (9) Step d. To prove Equation (9), we first prove the following fact: For each I I, there exists i I ω such that κ I(ϕ ω 1 )=κ I( π ii (ϕ i I 1 ) ) in P XI. (10) That is, the final sequence in P (Figure 1), when restricted to X I (that is FP), stabilizes within finitely many steps. Indeed, by Lemma 3.6, the ω op -limit ϕ ω 1 is described as an ω op -limit (i.e. an inf of a descending sequence) in P F ω 1: ϕ ω 1 = i ω π i (ϕ i 1 ). (11) Therefore, we have κ I (ϕω 1 )= i ω κ I π i (ϕi 1 ) since reindexing κ I preserves fibrewise limits. Here, the sequence ( κ I π i (ϕi 1 ) ) i ω in P X I is also descending. Therefore, by p

12 oinductive predicates and final sequences in a fibration 573 being a well-founded fibration (Definition 3.3) and X I being FP, there exists i I ω at which the descending sequence ( κ I π i (ϕi 1 ) ) i ω in P X I stabilizes, that is, κ ( I πi (ϕ i 1 ) ) = κ Iπi (ϕ i 1 )=κ I( π ii (ϕ i I 1 ) ) in P XI. i ω i ω ombined with Equation (11), this proves Equation (10). Step e. Finally, let us prove Equation (9). For each I I, (Fκ I ) ( b (ϕ ω 1 ) ) =(Fκ I ) ( b ( πi (ϕ i 1 ) )) by Equation (11) i ω = (Fκ I ) ( b ( πi (ϕ i 1 ) )) reindexing preserves i ω j ω(fκ I ) ( b ( π j+1(ϕ j+1 1 ) )) letting i = j +1fori 1 = j ω(fκ I ) ( (Fπ j ) (ϕ j+1 1 ) ) by π j+1 b = Fπ j (see Figure 1) = ϕ ( κ Iπj (ϕ j 1 ) ) by Definition 2.2 j ω ϕ ( κ Iπi I (ϕ i I 1 ) ) letting j = i I on the LHS = ϕ ( κ I(ϕ ω 1 ) ) by Equation (10) =(Fκ I ) (ϕ ω+1 1 ) by Definition 2.2 and ϕ ω+1 1 = ϕ(ϕ ω 1 ). This proves Equation (9) and concludes the proof of Lemma 3.7. The object ϕ ω 1 is a prototype of ϕ-coinductive predicates in various coalgebras. This is part of the main theorem below. It is standard that a coalgebra X c FX in induces a cone over the final F-sequence, and hence a mediating arrow X F ω 1 (see below). oncretely, c i : X F i 1 is defined inductively by X c 0 1is!;andc i+1 is the composite X c FX Fc i F i+1 1. The induced arrow to the limit F ω 1 is denoted by c ω. F ω 1 π i 1! F1 F i 1 c i X Note that F ω 1 does not necessarily carry a final F-coalgebra (see Remark 3.12). c ω (12) Theorem 3.9 (Main result). Let P p be a well-founded fibration; F : be a finitary functor; ϕ be a predicate lifting of F along p; andx c FX be a coalgebra in. 1. The ϕ-coinductive predicate νϕ c in c (Definition 2.3) exists. It is obtained by the following reindexing of ϕ ω 1,wherec ω is the mediating map in Equation (12). νϕ c = c ω(ϕ ω 1 ). (13)

13 I. Hasuo, T. Kataoka and K. ho Moreover, the predicate νϕ c is the limit of the following ω op -chain in the fibre P X X (c ϕ)( X ) (c ϕ) 2 ( X ), (14) that stabilizes after ω steps. That is, νϕ c = i ω (c ϕ) i ( X ). Proof. We proceed by steps. Step a. We first show that the descriptions of νϕ c in the items 1 2 are the same: c ω(ϕ ω 1 )= i ω(c ϕ) i ( X ). (15) We have ( c ω(ϕ ω 1 )=c ω πi (ϕ i 1 ) ) by Lemma 3.6 i ω = c ( ω π i (ϕ i 1 ) ) since reindexing preserves i ω = i ω c i (ϕ i 1 ) by the definition of c ω. (16) Furthermore, c i (ϕi 1 ) in the above is seen to be equal to (c ϕ) i ( X ). This is shown by induction on i ω. Fori = 0, the claim amounts to! ( 1 )= X, which holds since reindexing preserves. For the step case, c i+1(ϕ i+1 1 )=c (Fc i ) (ϕ i+1 1 ) by c i+1 = Fc i c = c ( ϕ ( c i (ϕ i 1 ) )) by Definition 2.2 =(c ϕ) ( (c ϕ) i ( X ) ) by induction hypothesis. Therefore the Equation (15) holds. Step b. In order to show that i ω (c ϕ) i ( X )istheϕ-coinductive predicate in c, we shall exhibit that the chain (14) the final (c ϕ)-sequence in P X stabilizes after ω steps. By Equation (15), the claim (c ϕ) ( i ω (c ϕ) i ( X ) ) = i ω (c ϕ) i ( X ) reduces to (c ϕ) ( c ω(ϕ ω 1 ) ) = c ω(ϕ ω 1 ). (17) Step c. Finally, we shall prove Equation (17): c ( ϕ(c ω(ϕ ω 1 )) ) = c ( (Fc ω ) (ϕ(ϕ ω 1 )) ) by Definition 2.2 = c ( (Fc ω ) (b (ϕ ω 1 )) ) by Lemma 3.7 =(b Fc ω c) (ϕ ω (18) 1 ) = c ω(ϕ ω 1 ). For the last equality, we used b Fc ω c = c ω, which is proved by showing that b Fc ω c is also a mediating map in Equation (12). Indeed, for each i 1, This concludes the proof. π i b Fc ω c = Fπ i 1 Fc ω c see Figure 1 = Fc i 1 c by Equation (12) = c i by the definition of c i.

14 oinductive predicates and final sequences in a fibration 575 Example 3.10 (Rν). We shall continue Example 2.4 and derive from Theorem 3.9 the behavioural bound result described in Section 1.1: the chain (2) stabilizes after ω steps, for each α Rν u and each finitely branching Kripke model c. Indeed, the latter is the same thing as a coalgebra X c F fbk X,whereF fbk = P(AP) P ω ( ). ompared to F K in Example 2.4, the powerset functor is restricted from P to P ω ; this makes F fbk a finitary functor. Still the same definition of ϕ α defines a predicate lifting of F fbk. Theorem can then be applied to the fibration Pred (easily seen to be Sets well-founded, Example 7.1), the finitary functor F fbk and the predicate lifting ϕ α for each α. It is not hard to see that the function [α] c : PX PX in Section 1.1 coincides with c ϕ α : Pred X Pred X (note that Pred X = 2 X = PX); thus the chain (2) coincides with Equation (14) that stabilizes after ω steps by Theorem 3.9. Remark The ω-bound of the length of the chain (14) is sharp. A (counter)example is given in the setting of Example 3.10, by the predicate lifting ϕ u and the coalgebra (i.e. Kripke structure) c 2 below. There b i,i has no successors. Indeed, while νϕ u c2 is {a i i ω}, itsith approximant ((c 2 ) i ϕ i u)( X ) in Equation (14) contains b i,0 too. c 2 a 0 b 0,0 a 1 b 1,0 b 1,1 a 2 b 2,0 b 2,1 b 2,2. Remark It is notable that Theorem 3.9 imposes no size restrictions on ϕ: P P. Being a predicate lifting is enough. To find an example such that ϕ is not finitary is future work. Our main theorem would not become trivial even if it turns out that ϕ is always finitary. Final F-sequences are commonly used for the construction of a final F-coalgebra. It is not always the case, however, that the limit F ω 1 is itself the carrier of a final coalgebra (even for finitary F; see Worrell (2005, Section 5)). One obtains a final coalgebra either by (1) quotienting F ω 1 by the behavioural equivalence (see e.g. Pattinson (2003)); or (2) continuing the final sequence till ω + ω steps. The latter construction is worked out

15 I. Hasuo, T. Kataoka and K. ho 576 in Worrell (2005) (in Sets) and in Adámek (2003) in LFP with additional assumptions. Its relevance to the current work is yet to be investigated. We emphasize that a final ϕ-sequence stabilizes in ω steps relatively to the underlying final F-sequence. In fact, we can also show that the final ϕ-sequence absolutely stabilizes in ω + ω steps for some LFP including Sets; a proof can be done by observing that the final ϕ-sequence stabilizes as soon as the final F-sequence stabilizes, once we are beyond ω steps. To show directly the stabilization of the final ϕ-sequence in ω + ω steps, one may want to prove that P is strongly LFP as in Adámek (2003) and that ϕ is finitary. Neither of these seems easy. oalgebra morphisms are compatible with coinductive predicates. This fact, like Proposition 2.5, is potentially useful in establishing coinductive predicates. Proposition Let f : X Y be a coalgebra morphism from X c FX to Y d FY. In the setting of Lemma 3.7 and Theorem 3.9: 1. If Q P Y is a ϕ-invariant in d, soisf Q P X in c. 2. We have νϕ c = f ( ) νϕ d. Proof. For the item 1, f Q f d (ϕq) Q is an invariant = c (Ff) (ϕq) f is a homomorphism = (c ϕ)(f Q) by Definition 2.2. For the item 2, the coalgebras give rise to mediating arrows X c ω F ω 1andY d ω F ω 1, respectively, as in Equation (12). It is easy to see that c ω = d ω f (using the universality of the limit F ω 1); using Equation (13) the claim follows. Remark The current paper focusses on FP objects, finitary functors, etc. i.e. the ω-presentable setting (see Adámek and Rosický (1994, Section 1.B)). This is for the simplicity of presentation: the results, as usual (as e.g. in Klin (2007)), can be easily generalized to the λ-presentable setting for an arbitrary regular cardinal λ. In such an extended setting, we obtain a behavioural λ-bound. 4. A fibration of invariants We organize the above observations in a more abstract fibred setting. The technical results are mostly standard; see e.g. Hermida (1993), Hermida and Jacobs (1998) and Jacobs (2012, hap.6). We write oalg(f) for the category of F-coalgebras. Proposition 4.1. Let ϕ be a predicate lifting of F along P p. Then the fibration P p is lifted oalg(ϕ) to a fibration p, with two forgetful functors forming a map of fibrations from the oalg(f) latter to the former.

16 oinductive predicates and final sequences in a fibration 577 Proof. It is easy to check each fibre oalg(ϕ) c is a poset. Let (X X c FX) f (Y FX FY )beanarrowinoalg(f), and P s ϕp be above Y d FY. A artesian lifting of f is obtained as in the following diagram: P ϕf P ϕf(p ) ϕp t s f P P f(p ) d FX c X Ff f FY Y d Here, we used the universality of the artesian lifting ϕf(p ) (see Definition 2.2). The two forgetful functors constitute a map of fibrations: The commutativity (5) is oalg(ϕ) obvious, and artesian liftings in p (which we constructed above) are based on the oalg(f) artesian liftings in P p. The next observation explains the current section s title. oalg(ϕ) Proposition 4.2. Let p be the lifted fibration in Proposition 4.1. For each coalgebra oalg(f) X c FX, the fibre over c coincides with the poset of ϕ-invariants in c. Thatis, = oalg(ϕ) c X oalg(c ϕ) FX. P X Proof. Given a ϕ-coalgebra P s ϕp above X c FX, we use the universality of the artesian lifting of c to obtain a (c ϕ)-coalgebra as in the following diagram: c (ϕp ) c(ϕp ) ϕp s P onversely, given a (c ϕ)-coalgebra Q X c FX as the following composite: t c (ϕq), we obtain a ϕ-coalgebra above c (ϕq) c(ϕq) ϕq t Q Then it is straightforward to see that the mappings are monotone and inverse to each other. The mappings commute with the forgetful functors since they do not change the carriers.

17 I. Hasuo, T. Kataoka and K. ho 578 oalg(ϕ) Therefore, Theorem and Proposition state the fibration p has fibrewise oalg(f) final objects. (At least part of) this statement itself is shown quite easily using the Knaster Tarski theorem (each fibre is a complete lattice). Our contribution is their concrete construction as ω op -limits (Theorem 3.9.2). The following lemma is essentially a special case of Lemma 3.6, but see also Jacobs (1999, Proposition and Exercise 9.2.4). Lemma 4.3. Let P p be a fibration; and assume that has a final object. Then P p has a fibrewise final object if and only if P has a final object that is above the final object of. oalg(ϕ) By applying the lemma to p, we obtain a basic relationship between coinductive oalg(f) predicates and final coalgebras. orollary 4.4. Let ϕ be a predicate lifting of F along P p; and assume that a final F-coalgebra exists. The following are equivalent: 1. The coinductive predicate νϕ c exists for each coalgebra c: X FX. Moreover, they are preserved by reindexing (along coalgebra morphisms). 2. There exists a final ϕ-coalgebra that is above the final F-coalgebra. As noted in Remark 3.12, however, our concrete construction of coinductive predicates does not rely on a final F-coalgebra. 5. Inductive predicates over coinductive datatypes The central topic of the current paper is coinductive predicates over coinductive datatypes, the latter identified as coalgebras in the base category of a fibration P p. Some variations are possible, namely: inductive/coinductive predicates over inductive/coinductive datatypes. For example, Hermida and Jacobs (1998) focus on: inductive predicates over inductive datatypes (the latter identified as algebras); and coinductive predicates over coinductive datatypes (as we have done in the previous sections). It turns out that, among these four variations, inductive predicates over coinductive datatypes allow a straightforward adaptation of our current categorical framework by P (op) taking the fibrewise opposite p (op) of the fibration P p we are interested in. We present these results in the current section. The study of the other two variations inductive predicates over inductive datatypes, and coinductive predicates over inductive datatypes is left as future work. In fact, we have preliminary observations that under certain assumptions these two variations coincide. Their details will be presented in another venue. The following is the definition of an inductive predicate (on a coinductive datatype). It is not hard to see that the definition generalizes e.g. the semantics of the μ operator of the modal μ-calculus in a Kripke model. Later in Lemma 5.4, we will identify it as a coinductive predicate in the fibrewise opposite.

18 oinductive predicates and final sequences in a fibration 579 Definition 5.1 (Inductive predicate). Let ϕ be a predicate lifting along a fibration P p ;and X c FX be a coalgebra in. Theϕ-inductive predicate in c is the initial (c ϕ)-algebra (if it exists). We denote its carrier by μϕ c. Hence, it is the smallest predicate P P X such that P c (ϕp )inp X. P (op) In what follows we utilize the notion of fibrewise opposite p (op) of a fibration P p (Bénabou (1975); see also (Jacobs 1999, Definition )). Intuitively, the fibrewise opposite p (op) is obtained by opposing the order in each fibre P X but leaving the base category, as well as the reindexing structure, as in the original fibration p. The precise definition is best stated via indexed categories and the Grothendieck construction. It is left to the appendix (Lemma.13). P (op) Some remarks are in order. First, the total category P (op) of the fibrewise opposite p (op) is in general different from the opposite category P op (in the usual sense) of P. The same applies to the functor p (op), that is different from the opposite functor p op. We emphasize P (op) p (op) that in the fibrewise opposite P (op) p (op), the base category stays the same. We also note that is a fibration, unlike the opposite functor P op p op of p that is canonically an opfibration. op Notation 5.2. For distinction, we denote reindexing functors in fibrations P P (op) p and p (op) by f and f #, respectively. They are in fact the same monotone functions between fibres as posets: (P (op) ) Y f # (P (op) ) X (P Y ) op (f ) op (PX ) op for f : X Y. The following result, although straightforward, is essential for the subsequent technical development. Lemma 5.3. Let P p be a fibration and F be an endofunctor on. For a predicate lifting ϕ: P P of F along p, there exists a canonical predicate lifting ϕ (op) : P (op) P (op), P (op) which we call the fibrewise opposite of ϕ, off along the fibration p (op). Proof. We give an explicit construction here, although the statement is almost trivial when stated in terms of indexed categories. On objects, we define ϕ (op) P = ϕp. For the action on arrows, we first note that an arrow P Q in P (op) above f : X Y exists if and only if P f # Q in (P (op) ) X =(P X ) op. Exploiting this fact, ϕ (op) s action on the arrow P Q is defined to be the unique arrow ϕ (op) P ϕ (op) Q above Ff: FX FY. The last (unique) arrow exists, indeed: We have ϕ (op) P (Ff) # ϕ (op) Q in (P (op) ) FX by ϕp ϕf Q =(Ff) ϕq in P FX. Here, the last equality is because ϕ is a predicate lifting.

19 I. Hasuo, T. Kataoka and K. ho 580 Lemma 5.4. Let P be a predicate over X. 1. The object P P X carries a (c ϕ)-algebra if and only if P (P X ) op =(P (op) ) X is a ϕ (op) -invariant in c. 2. The ϕ-inductive predicate in c is the ϕ (op) -coinductive predicate in c. Thatis,μϕ c = ν(ϕ (op) ) c as objects in P X. Proof. The category of (c ϕ)-algebras in P X is dually equivalent to the category of (c # ϕ (op) )-coalgebras in (P (op) ) X, since the following diagram (in Posets) commutes. (P (op) ) X (ϕ (op) ) X (P (op) ) FX c # (P (op) ) X (P X ) op ϕ op X (P FX ) op (c ) op (P X ) op Thanks to the previous characterization inductive predicates in P p as coinductive ones P (op) in p (op) we can apply all the results that we have obtained so far to inductive predicates. Notice again that the base category has remained the same. The characterization in Lemma 5.4 can be seen as a generalization of the duality μu. ϕ(u) = νu. ϕ( u) between least and greatest fixed points in classical logics the latter is a special case where fibres are self-dual, i.e. P P (op) p = p (op). Via the last characterization, our main result (Theorem 3.9) can also be used to show the stabilization of the ω-chain when calculating inductive predicates (see orollary 5.8). The inductive predicate on F ω 1 is not a limit nor a colimit in P, but it is a limit in P (op) (see Definition 5.7). Definition 5.5 (o-well-founded fibration). A co-well-founded fibration is a finitely determined fibration that further satisfies: 3.3. If X F (hence FP), the fibre P X is such that: the category P X consists solely of FP objects. Since P X is cocomplete, this is equivalent to: there is no (ω-)chain P 0 <P 1 < in P X that is strictly ascending. Lemma 5.6. For a finitely determined fibration P P (op) p, its fibrewise opposite p (op) is also finitely determined. Moreover, p (op) is well-founded if and only if the fibration p is cowell-founded. Proof. It is trivial that the fibration p (op) satisfies the condition 1 (of Definition 3.2) if and only if p satisfies it. For the condition 2, p (op) has fibrewise limits and colimits, because p has fibrewise colimits and limits, respectively. The condition 3 for p (op) is obviously equivalent to the one for p since reindexing functors κ I,κ# I are the same as functions. By (P (op) ) X =(P X ) op, p (op) satisfies the condition 3.3 if and only if p satisfies 3.3.

20 oinductive predicates and final sequences in a fibration 581 Definition 5.7. Let 1 be the least element of the fibre P 1 (hence the greatest in (P (op) ) 1 ). We denote by ϕ ω 1 P F ω 1 the limit of the following diagram in P (op). It is easily seen to reside above the final F-sequence in. 1 ϕ 1 ϕ i 1 in P (op) Note here that 1 is the final object in P (op), and the object ϕ 1 is the functor ϕ (op) applied to 1. Therefore, the above diagram is the final ϕ (op) -sequence in P (op). Using Lemma 3.6, it is not hard to see that ϕ ω 1 = i ω π i (ϕi 1 ) in the fibration P p, where (π i : F ω 1 F i 1) i ω is the limiting cone for the final F-sequence in. The following is our main result adapted to inductive predicates. In particular, it states that an inductive predicate is computed as a supremum of an ω-chain. orollary 5.8. Let P p be a co-well-founded fibration; F : be a finitary functor; ϕ be a predicate lifting of F along p; andx c FX be a coalgebra in. 1. The ϕ-inductive predicate μϕ c in c exists. It is obtained by the following reindexing of ϕ ω 1,wherec ω is the mediating map in Equation (12). μϕ c = c ω(ϕ ω 1 ) 2. Moreover, the predicate μϕ c is the colimit of the following ω-chain in the fibre P X X (c ϕ)( X ) (c ϕ) 2 ( X ), that stabilizes after ω steps. That is, μϕ c = i ω (c ϕ) i ( X ). Proof. By Lemmas 5.4 and 5.6 and Theorem 3.9. orollary 5.9. Let ϕ be a predicate lifting of F along P (oalg(ϕ(op)))(op) p;and p (op)(op) be the fibrewise oalg(f) P (op) opposite of the lift of the fibration p (op) (see Proposition 4.1 and Lemma 5.3). For each coalgebra X c FX, the following diagram commutes: ( (oalg(ϕ (op) ) ) ) (op) X FX c ((P X ) op ) op = Alg(c ϕ) P X Proof. Apply Proposition 4.2 for the predicate lifting ϕ (op) along oalg(ϕ (op) ) X c FX P (op) p (op) = oalg(c # ϕ (op) ), (P (op) ) X whose opposite categories are the ones in the diagram we want to prove., we obtain

21 I. Hasuo, T. Kataoka and K. ho 582 oalgebra morphisms are compatible with inductive predicates just as in Proposition Therefore, the inductive predicates μϕ c form a fibrewise initial object = μϕ of the fibration p (op)(op). 6. Examples at large Here are several results that ensure a fibration to be finitely determined or well-founded, and hence enable us to apply Theorem 3.9. Some of them are well-known; others especially those which relate fibrations and locally (finitely) presentable categories, including Lemmas 6.3 and 6.7 seem to be new. The following results provide sufficient conditions for a fibration to be finitely determined (Definition 3.2). Recall that a full subcategory F of P is said to be dense if each object P P is a colimit of the canonical diagram F/P π F P. Lemma 6.1. Let P p be a fibration with fibrewise limits and colimits and coproducts between fibres. Assume further that is LFP with a set F of FP objects (as in Definition 3.1). If the total category P has a dense subcategory F P such that every R F P is above F (i.e. pr F ), then p is finitely determined. Proof. The only non-trivial part is the direction of ond. 3. For that, it suffices to show that arbitrary P P is a colimit of the diagram (κ I P ). Here, I and κ I are as in ond. 3. By Lemma.11, the colimit olim κ I P is described as κ I κ I P using a sup in κ I P X, since (X I X) is colimiting. We have κ I κ IP P as a counit of an adjunction; therefore, olim κ I P P. Thus, it suffices to show that P olim κ I P in P X.Let(P J ) J J be a diagram in P g J such that P J F P and there is a colimiting cocone (P J P )J J. Such a diagram exists since F P is dense. By the assumption, for each J, the object P J F P lies above an object in F. Therefore, the arrow pg J : pp J pp = X is an object of F /X; since I = F /X, wecanchoose g J I J I such that κ IJ = pg J. Now an arrow P J P in P induces P J (pg J ) P = κ I J P (19) by the universality of artesian arrows. We proceed as follows: P = olim P ( ) J = ( ) pg J J J P J κ IJ κ I J P κ I κ IP ( ) = olim κ IP. J J J J For ( ), we used Lemma.11; ( ) holds since I J is chosen so that κ IJ = pg J and Equation (19) hold. This concludes the proof. orollary 6.2. Let P p be a fibration with fibrewise limits and colimits and coproducts between fibres, where is LFP with a set F of FP objects (in Definition 3.1). If the total category P is also LFP, with a set F P of FP objects (as in Definition 3.1) chosen so that every R F P is above F, then p is finitely determined.

22 oinductive predicates and final sequences in a fibration Subobject fibrations The following is one of the results that are non-trivial. Lemma 6.3. Let be an LFP category with F being a set of FP objects (as in Definition 3.1). Then the total category Sub() of the subobject fibration is LFP: the set F Sub() := {(P X) X F, and there exists a strong epi Z P such that Z F} consists of FP objects in Sub(); and every object (Q Y ) Sub() is a colimit of a filtered diagram in F Sub(). Proof. The proof is by steps. Step a. First, we show that Sub() is complete and cocomplete. We rely on Lemma.11. Sub() We start with fibrewise limits in ; the proof is like in Jacobs (1999, Example 1.8.3(iii)). By Lemma B.6, an LFP category is complete. This equips each fibre Sub(X) with arbitrary inf s computed as wide pullbacks. A reindexing functor (by pullbacks) preserves these inf s since limits commute. Therefore, by Lemma.11, the total category Sub() is complete. Each fibre (which is a poset) has arbitrary inf s; hence, it is a complete lattice and arbitrary sup s also exist. Sub() Next, we show that is a bifibration (Definition.3). An abstract proof can be given by Freyd s adjoint functor theorem (note that each fibre Sub(X) is a complete lattice, and that reindexing f preserves inf s). Instead we explicitly introduce exploiting a factorization structure of LFP (Lemma B.6.2). Namely, given (P m X) Sub(X) and f : X Y, the opreindexing f P is defined by the (StrongEpi, Mono)-factorization of f m, asbelow. P f P m (20) X Y f The fact that f P Q if and only if P f Q is easily proved using the diagonalization property of the factorization structure. This establishes f as a left adjoint to reindexing f. Using Lemma.11, we conclude that Sub() is cocomplete. Step b. Let Im: /Y Sub(Y ) be the image functor defined by the (StrongEpi, Mono)- factorization (i.e. Im f = f X for f : X Y ). In the notation in Lemma B.11.2, we have F Sub() = {Im f X F, f F/X} = {(P X) Sub() X F, P F Sub(X) }. The set F Sub() is small, since F is small and F Sub(X) is small for each X F. Step c. First, we prove that (P m X) F Sub() is FP in Sub(). Opreindexings f f do not have to satisfy the Beck hevalley condition.

Knowledge and its Place in Nature by Hilary Kornblith

Knowledge and its Place in Nature by Hilary Kornblith Deduction by Daniel Bonevac Chapter 7 Quantified Natural Deduction Quantified Natural Deduction As with truth trees, natural deduction in Q depends on the addition of some new rules to handle the quantifiers.

More information

ENGG1410-F Tutorial 6

ENGG1410-F Tutorial 6 Jianwen Zhao Department of Computer Science and Engineering The Chinese University of Hong Kong 1/16 Problem 1. Matrix Diagonalization Diagonalize the following matrix: A = [ ] 1 2 4 3 2/16 Solution The

More information

國家圖書館典藏電子全文

國家圖書館典藏電子全文 i ii Abstract The most important task in human resource management is to encourage and help employees to develop their potential so that they can fully contribute to the organization s goals. The main

More information

10384 19020101152519 UDC Rayleigh Quasi-Rayleigh Method for computing eigenvalues of symmetric tensors 2 0 1 3 2 0 1 3 2 0 1 3 2013 , 1. 2. [4], [27].,. [6] E- ; [7], Z-. [15]. Ramara G. kolda [1, 2],

More information

Microsoft Word - TIP006SCH Uni-edit Writing Tip - Presentperfecttenseandpasttenseinyourintroduction readytopublish

Microsoft Word - TIP006SCH Uni-edit Writing Tip - Presentperfecttenseandpasttenseinyourintroduction readytopublish 我 难 度 : 高 级 对 们 现 不 在 知 仍 道 有 听 影 过 响 多 少 那 次 么 : 研 英 究 过 文 论 去 写 文 时 作 的 表 技 引 示 巧 言 事 : 部 情 引 分 发 言 该 生 使 在 中 用 过 去, 而 现 在 完 成 时 仅 表 示 事 情 发 生 在 过 去, 并 的 哪 现 种 在 时 完 态 成 呢 时? 和 难 过 道 去 不 时 相 关? 是 所 有

More information

Microsoft PowerPoint _代工實例-1

Microsoft PowerPoint _代工實例-1 4302 動態光散射儀 (Dynamic Light Scattering) 代工實例與結果解析 生醫暨非破壞性分析團隊 2016.10 updated Which Size to Measure? Diameter Many techniques make the useful and convenient assumption that every particle is a sphere. The

More information

國立中山大學學位論文典藏

國立中山大學學位論文典藏 I II III IV The theories of leadership seldom explain the difference of male leaders and female leaders. Instead of the assumption that the leaders leading traits and leading styles of two sexes are the

More information

Microsoft Word - A200811-773.doc

Microsoft Word - A200811-773.doc 语 言 模 型 在 高 校 保 研 工 作 中 的 应 用 王 洋 辽 宁 工 程 技 术 大 学 理 学 院 信 息 与 计 算 科 学, 辽 宁 阜 新 (3000) E-mail: ben.dan000 @63.com 摘 要 : 问 题 重 述 : 模 糊 性 数 学 发 展 的 主 流 是 在 它 的 应 用 方 面, 其 中 模 糊 语 言 模 型 实 现 了 人 类 语 言 的 数 学

More information

untitled

untitled Co-integration and VECM Yi-Nung Yang CYCU, Taiwan May, 2012 不 列 1 Learning objectives Integrated variables Co-integration Vector Error correction model (VECM) Engle-Granger 2-step co-integration test Johansen

More information

<4D6963726F736F667420576F7264202D2032303130C4EAC0EDB9A4C0E04142BCB6D4C4B6C1C5D0B6CFC0FDCCE2BEABD1A15F325F2E646F63>

<4D6963726F736F667420576F7264202D2032303130C4EAC0EDB9A4C0E04142BCB6D4C4B6C1C5D0B6CFC0FDCCE2BEABD1A15F325F2E646F63> 2010 年 理 工 类 AB 级 阅 读 判 断 例 题 精 选 (2) Computer mouse How does the mouse work? We have to start at the bottom, so think upside down for now. It all starts with mouse ball. As the mouse ball in the bottom

More information

東吳大學

東吳大學 律 律 論 論 療 行 The Study on Medical Practice and Coercion 林 年 律 律 論 論 療 行 The Study on Medical Practice and Coercion 林 年 i 讀 臨 療 留 館 讀 臨 律 六 礪 讀 不 冷 療 臨 年 裡 歷 練 禮 更 老 林 了 更 臨 不 吝 麗 老 劉 老 論 諸 見 了 年 金 歷 了 年

More information

中国科学技术大学学位论文模板示例文档

中国科学技术大学学位论文模板示例文档 University of Science and Technology of China A dissertation for doctor s degree An Example of USTC Thesis Template for Bachelor, Master and Doctor Author: Zeping Li Speciality: Mathematics and Applied

More information

國立中山大學學位論文典藏.PDF

國立中山大學學位論文典藏.PDF I II III The Study of Factors to the Failure or Success of Applying to Holding International Sport Games Abstract For years, holding international sport games has been Taiwan s goal and we are on the way

More information

BC04 Module_antenna__ doc

BC04 Module_antenna__ doc http://www.infobluetooth.com TEL:+86-23-68798999 Fax: +86-23-68889515 Page 1 of 10 http://www.infobluetooth.com TEL:+86-23-68798999 Fax: +86-23-68889515 Page 2 of 10 http://www.infobluetooth.com TEL:+86-23-68798999

More information

國立中山大學學位論文典藏.PDF

國立中山大學學位論文典藏.PDF 中 國 文 學 系 國 立 中 山 大 學, 碩 士 論 文 國 立 中 山 大 學 中 國 文 學 系 碩 士 論 文 Department of Chinese Literature 肉 蒲 團 研 究 National Sun Yat-sen University Master Thesis 肉 蒲 團 研 究 The Research of Rou Pu Tuan 研 究 生 : 林 欣 穎

More information

UDC The Policy Risk and Prevention in Chinese Securities Market

UDC The Policy Risk and Prevention in Chinese Securities Market 10384 200106013 UDC The Policy Risk and Prevention in Chinese Securities Market 2004 5 2004 2004 2004 5 : Abstract Many scholars have discussed the question about the influence of the policy on Chinese

More information

Improved Preimage Attacks on AES-like Hash Functions: Applications to Whirlpool and Grøstl

Improved Preimage Attacks on AES-like Hash Functions: Applications to Whirlpool and Grøstl SKLOIS (Pseudo) Preimage Attack on Reduced-Round Grøstl Hash Function and Others Shuang Wu, Dengguo Feng, Wenling Wu, Jian Guo, Le Dong, Jian Zou March 20, 2012 Institute. of Software, Chinese Academy

More information

A VALIDATION STUDY OF THE ACHIEVEMENT TEST OF TEACHING CHINESE AS THE SECOND LANGUAGE by Chen Wei A Thesis Submitted to the Graduate School and Colleg

A VALIDATION STUDY OF THE ACHIEVEMENT TEST OF TEACHING CHINESE AS THE SECOND LANGUAGE by Chen Wei A Thesis Submitted to the Graduate School and Colleg 上 海 外 国 语 大 学 SHANGHAI INTERNATIONAL STUDIES UNIVERSITY 硕 士 学 位 论 文 MASTER DISSERTATION 学 院 国 际 文 化 交 流 学 院 专 业 汉 语 国 际 教 育 硕 士 题 目 届 别 2010 届 学 生 陈 炜 导 师 张 艳 莉 副 教 授 日 期 2010 年 4 月 A VALIDATION STUDY

More information

1 * 1 *

1 * 1 * 1 * 1 * taka@unii.ac.jp 1992, p. 233 2013, p. 78 2. 1. 2014 1992, p. 233 1995, p. 134 2. 2. 3. 1. 2014 2011, 118 3. 2. Psathas 1995, p. 12 seen but unnoticed B B Psathas 1995, p. 23 2004 2006 2004 4 ah

More information

<4D6963726F736F667420576F7264202D203338B4C12D42A448A4E5C3C0B34EC3FE2DAB65ABE1>

<4D6963726F736F667420576F7264202D203338B4C12D42A448A4E5C3C0B34EC3FE2DAB65ABE1> ϲ ฯ र ቑ ጯ 高雄師大學報 2015, 38, 63-93 高雄港港史館歷史變遷之研究 李文環 1 楊晴惠 2 摘 要 古老的建築物往往承載許多回憶 也能追溯某些歷史發展的軌跡 位於高雄市蓬 萊路三號 現為高雄港港史館的紅磚式建築 在高雄港三號碼頭作業區旁的一片倉庫 群中 格外搶眼 這棟建築建成於西元 1917 年 至今已將近百年 不僅躲過二戰戰 火無情轟炸 並保存至今 十分可貴 本文透過歷史考證

More information

PowerPoint Presentation

PowerPoint Presentation ITM omputer and ommunication Technologies Lecture #4 Part I: Introduction to omputer Technologies Logic ircuit Design & Simplification ITM 計算機與通訊技術 2 23 香港中文大學電子工程學系 Logic function implementation Logic

More information

9 * B0-0 * 16ZD097 10 2018 5 3 11 117 2011 349 120 121 123 46 38-39 12 2018 5 23 92 939 536 2009 98 1844 13 1 25 926-927 3 304 305-306 1 23 95 14 2018 5 25 926-927 122 1 1 self-ownership 15 22 119 a b

More information

摘 要 張 捷 明 是 台 灣 當 代 重 要 的 客 語 兒 童 文 學 作 家, 他 的 作 品 記 錄 著 客 家 人 的 思 想 文 化 與 觀 念, 也 曾 榮 獲 多 項 文 學 大 獎 的 肯 定, 對 台 灣 這 塊 土 地 上 的 客 家 人 有 著 深 厚 的 情 感 張 氏 於

摘 要 張 捷 明 是 台 灣 當 代 重 要 的 客 語 兒 童 文 學 作 家, 他 的 作 品 記 錄 著 客 家 人 的 思 想 文 化 與 觀 念, 也 曾 榮 獲 多 項 文 學 大 獎 的 肯 定, 對 台 灣 這 塊 土 地 上 的 客 家 人 有 著 深 厚 的 情 感 張 氏 於 玄 奘 大 學 中 國 語 文 學 系 碩 士 論 文 客 家 安 徒 生 張 捷 明 童 話 研 究 指 導 教 授 : 羅 宗 濤 博 士 研 究 生 : 黃 春 芳 撰 中 華 民 國 一 0 二 年 六 月 摘 要 張 捷 明 是 台 灣 當 代 重 要 的 客 語 兒 童 文 學 作 家, 他 的 作 品 記 錄 著 客 家 人 的 思 想 文 化 與 觀 念, 也 曾 榮 獲 多 項 文

More information

Stochastic Processes (XI) Hanjun Zhang School of Mathematics and Computational Science, Xiangtan University 508 YiFu Lou talk 06/

Stochastic Processes (XI) Hanjun Zhang School of Mathematics and Computational Science, Xiangtan University 508 YiFu Lou talk 06/ Stochastic Processes (XI) Hanjun Zhang School of Mathematics and Computational Science, Xiangtan University hjzhang001@gmail.com 508 YiFu Lou talk 06/04/2010 - Page 1 Outline 508 YiFu Lou talk 06/04/2010

More information

UDC Empirical Researches on Pricing of Corporate Bonds with Macro Factors 厦门大学博硕士论文摘要库

UDC Empirical Researches on Pricing of Corporate Bonds with Macro Factors 厦门大学博硕士论文摘要库 10384 15620071151397 UDC Empirical Researches on Pricing of Corporate Bonds with Macro Factors 2010 4 Duffee 1999 AAA Vasicek RMSE RMSE Abstract In order to investigate whether adding macro factors

More information

Microsoft Word doc

Microsoft Word doc 中 考 英 语 科 考 试 标 准 及 试 卷 结 构 技 术 指 标 构 想 1 王 后 雄 童 祥 林 ( 华 中 师 范 大 学 考 试 研 究 院, 武 汉,430079, 湖 北 ) 提 要 : 本 文 从 结 构 模 式 内 容 要 素 能 力 要 素 题 型 要 素 难 度 要 素 分 数 要 素 时 限 要 素 等 方 面 细 致 分 析 了 中 考 英 语 科 试 卷 结 构 的

More information

Microsoft PowerPoint - STU_EC_Ch08.ppt

Microsoft PowerPoint - STU_EC_Ch08.ppt 樹德科技大學資訊工程系 Chapter 8: Counters Shi-Huang Chen Fall 2010 1 Outline Asynchronous Counter Operation Synchronous Counter Operation Up/Down Synchronous Counters Design of Synchronous Counters Cascaded Counters

More information

Untitled-3

Untitled-3 SEC.. Separable Equations In each of problems 1 through 8 solve the given differential equation : ü 1. y ' x y x y, y 0 fl y - x 0 fl y - x 0 fl y - x3 3 c, y 0 ü. y ' x ^ y 1 + x 3 x y 1 + x 3, y 0 fl

More information

Microsoft Word - 第四組心得.doc

Microsoft Word - 第四組心得.doc 徐 婉 真 這 四 天 的 綠 島 人 權 體 驗 營 令 我 印 象 深 刻, 尤 其 第 三 天 晚 上 吳 豪 人 教 授 的 那 堂 課, 他 讓 我 聽 到 不 同 於 以 往 的 正 義 之 聲 轉 型 正 義, 透 過 他 幽 默 熱 情 的 語 調 激 起 了 我 對 政 治 的 興 趣, 願 意 在 未 來 多 關 心 社 會 多 了 解 政 治 第 一 天 抵 達 綠 島 不 久,

More information

59-81

59-81 BIBLID 0254-4466(2001)19:2 pp. 59-81 19 2 90 12 * 59 60 19 2 1498-1583 6 1572 12 27 1525-1582 1572-1620 1368-1398 1426-1435 1450-1456 1610-1695 15 1538-1588 1535-1608 61 1 1503-1583 1516-1591 1472-1528

More information

Shanghai International Studies University THE STUDY AND PRACTICE OF SITUATIONAL LANGUAGE TEACHING OF ADVERB AT BEGINNING AND INTERMEDIATE LEVEL A Thes

Shanghai International Studies University THE STUDY AND PRACTICE OF SITUATIONAL LANGUAGE TEACHING OF ADVERB AT BEGINNING AND INTERMEDIATE LEVEL A Thes 上 海 外 国 语 大 学 硕 士 学 位 论 文 对 外 汉 语 初 中 级 副 词 情 境 教 学 研 究 与 实 践 院 系 : 国 际 文 化 交 流 学 院 学 科 专 业 : 汉 语 国 际 教 育 姓 名 : 顾 妍 指 导 教 师 : 缪 俊 2016 年 5 月 Shanghai International Studies University THE STUDY AND PRACTICE

More information

A Community Guide to Environmental Health

A Community Guide to Environmental Health 102 7 建 造 厕 所 本 章 内 容 宣 传 推 广 卫 生 设 施 104 人 们 需 要 什 么 样 的 厕 所 105 规 划 厕 所 106 男 女 对 厕 所 的 不 同 需 求 108 活 动 : 给 妇 女 带 来 方 便 110 让 厕 所 更 便 于 使 用 111 儿 童 厕 所 112 应 急 厕 所 113 城 镇 公 共 卫 生 设 施 114 故 事 : 城 市 社

More information

東莞工商總會劉百樂中學

東莞工商總會劉百樂中學 /2015/ 頁 (2015 年 版 ) 目 錄 : 中 文 1 English Language 2-3 數 學 4-5 通 識 教 育 6 物 理 7 化 學 8 生 物 9 組 合 科 學 ( 化 學 ) 10 組 合 科 學 ( 生 物 ) 11 企 業 會 計 及 財 務 概 論 12 中 國 歷 史 13 歷 史 14 地 理 15 經 濟 16 資 訊 及 通 訊 科 技 17 視 覺

More information

<4D6963726F736F667420506F776572506F696E74202D20B5DAD2BBD5C228B4F2D3A1B0E6292E707074205BBCE6C8DDC4A3CABD5D>

<4D6963726F736F667420506F776572506F696E74202D20B5DAD2BBD5C228B4F2D3A1B0E6292E707074205BBCE6C8DDC4A3CABD5D> Homeworks ( 第 三 版 ):.4 (,, 3).5 (, 3).6. (, 3, 5). (, 4).4.6.7 (,3).9 (, 3, 5) Chapter. Number systems and codes 第 一 章. 数 制 与 编 码 . Overview 概 述 Information is of digital forms in a digital system, and

More information

PowerPoint Presentation

PowerPoint Presentation Decision analysis 量化決策分析方法專論 2011/5/26 1 Problem formulation- states of nature In the decision analysis, decision alternatives are referred to as chance events. The possible outcomes for a chance event

More information

不确定性环境下公司并购的估价:一种实物期权.doc

不确定性环境下公司并购的估价:一种实物期权.doc Abstract In view of the inadequacy of investment valuation under uncertainty by the orthodox discounted cash flow (DCF), many scholars have begun to study the investment under uncertainty. Option pricing

More information

<4D6963726F736F667420576F7264202D203033BDD7A16DA576B04FA145A4ADABD2A5BBACF6A16EADBAB6C0ABD2A4A7B74EB8712E646F63>

<4D6963726F736F667420576F7264202D203033BDD7A16DA576B04FA145A4ADABD2A5BBACF6A16EADBAB6C0ABD2A4A7B74EB8712E646F63> 論 史 記 五 帝 本 紀 首 黃 帝 之 意 義 林 立 仁 明 志 科 技 大 學 通 識 教 育 中 心 副 教 授 摘 要 太 史 公 司 馬 遷 承 父 著 史 遺 志, 並 以 身 膺 五 百 年 大 運, 上 繼 孔 子 春 秋 之 史 學 文 化 道 統 為 其 職 志, 著 史 記 欲 達 究 天 人 之 際, 通 古 今 之 變, 成 一 家 之 言 之 境 界 然 史 記 百

More information

Journal of Hangzhou Normal University Humanities and Social Sciences No. 6 Nov ! / % & 2 PP P. 9

Journal of Hangzhou Normal University Humanities and Social Sciences No. 6 Nov ! / % & 2 PP P. 9 詹 康 11605 B223. 5 A 1674-2338 2017 06-0009 -25 DOI 10. 3969/ j. issn. 1674-2338. 2017. 06. 002 1 P. 409 507 5181 1 2017-05-26 1 1961 1988 9 2017 11 6 Journal of Hangzhou Normal University Humanities and

More information

HPM 通 訊 第 八 卷 第 二 三 期 合 刊 第 二 版 數 學 歸 納 法 是 什 麼 玩 意 兒 中 原 大 學 師 資 培 育 中 心 楊 凱 琳 教 授 一 數 學 歸 納 法 不 同 於 歸 納 法 數 學 歸 納 法 在 數 學 知 識 的 領 域 中, 是 屬 於 基 本 原 理

HPM 通 訊 第 八 卷 第 二 三 期 合 刊 第 二 版 數 學 歸 納 法 是 什 麼 玩 意 兒 中 原 大 學 師 資 培 育 中 心 楊 凱 琳 教 授 一 數 學 歸 納 法 不 同 於 歸 納 法 數 學 歸 納 法 在 數 學 知 識 的 領 域 中, 是 屬 於 基 本 原 理 HPM 通 訊 第 八 卷 第 二 三 期 合 刊 第 一 版 數 學 歸 納 法 專 輯 發 行 人 : 洪 萬 生 ( 台 灣 師 大 數 學 系 教 授 ) 主 編 : 蘇 惠 玉 ( 西 松 高 中 ) 副 主 編 : 林 倉 億 ( 台 師 大 數 學 系 ) 助 理 編 輯 : 張 復 凱 歐 士 福 ( 台 灣 師 大 數 學 所 ) 編 輯 小 組 : 蘇 意 雯 ( 成 功 高 中

More information

A Study on the Relationships of the Co-construction Contract A Study on the Relationships of the Co-Construction Contract ( ) ABSTRACT Co-constructio in the real estate development, holds the quite

More information

A Study of Su Hsuei-Lin s Painting Based on the Literati Painting Prototype Wu Rong-Fu Assistant Professor, Department of Chinese Literature, National

A Study of Su Hsuei-Lin s Painting Based on the Literati Painting Prototype Wu Rong-Fu Assistant Professor, Department of Chinese Literature, National 2007 4 131-170 prototype theory 131 A Study of Su Hsuei-Lin s Painting Based on the Literati Painting Prototype Wu Rong-Fu Assistant Professor, Department of Chinese Literature, National Cheng Kung University

More information

<4D6963726F736F667420576F7264202D20D0ECB7C9D4C6A3A8C5C5B0E6A3A92E646F63>

<4D6963726F736F667420576F7264202D20D0ECB7C9D4C6A3A8C5C5B0E6A3A92E646F63> 硕 士 专 业 学 位 论 文 论 文 题 目 性 灵 文 学 思 想 与 高 中 作 文 教 学 研 究 生 姓 名 指 导 教 师 姓 名 专 业 名 称 徐 飞 云 卞 兆 明 教 育 硕 士 研 究 方 向 学 科 教 学 ( 语 文 ) 论 文 提 交 日 期 2012 年 9 月 性 灵 文 学 思 想 与 高 中 作 文 教 学 中 文 摘 要 性 灵 文 学 思 想 与 高 中 作

More information

2009.05

2009.05 2009 05 2009.05 2009.05 璆 2009.05 1 亿 平 方 米 6 万 套 10 名 20 亿 元 5 个 月 30 万 亿 60 万 平 方 米 Data 围 观 CCDI 公 司 内 刊 企 业 版 P08 围 观 CCDI 管 理 学 上 有 句 名 言 : 做 正 确 的 事, 比 正 确 地 做 事 更 重 要 方 向 的 对 错 于 大 局 的 意 义 而 言,

More information

2006 3,,,,,, :, : ( [1996 ]1998 :396) : ( [1998 ]1999 :274), :,,,,,,,,,,,,,,,,, ([1962 ]1993 : ),,( ),,,, concordiadiscors ( ) 2, 2,,,, ( ),,,,

2006 3,,,,,, :, : ( [1996 ]1998 :396) : ( [1998 ]1999 :274), :,,,,,,,,,,,,,,,,, ([1962 ]1993 : ),,( ),,,, concordiadiscors ( ) 2, 2,,,, ( ),,,, : 2006 3 Society 26 :,,,,,, :,,,,,, :,,, : ; ;,,,,; ([1951 ]1991 :16), :,,, (, [ 1971 ] 1988) 1,,,,,, E 1,,,, 1 2006 3,,,,,, :, : ( [1996 ]1998 :396) : ( [1998 ]1999 :274), :,,,,,,,,,,,,,,,,, ([1962 ]1993

More information

32 戲劇學刊 A Study of Beijing Opera s Jing Actors and Their Vocal Accents in the Early Twentieth Century Using Two Operas, Muhuguan and Yuguoyuan, as Exa

32 戲劇學刊 A Study of Beijing Opera s Jing Actors and Their Vocal Accents in the Early Twentieth Century Using Two Operas, Muhuguan and Yuguoyuan, as Exa 李元皓 二十世紀初期京劇淨行演員及其唱腔研究 以 牧虎關 御果園 為例 二十世紀初期京劇淨行演員及其唱腔研 究 以 牧虎關 御果園 為例* 李元皓** 中文摘要 形成於十九世紀的京劇 在二十世紀初時 發展的勢頭風潮臻於極盛 新興 的唱片錄音科技也於十九世紀末抵達中國 留下了一批珍貴的老唱片 以不同於 書面文字的方式 記錄著京劇有聲的過往 老唱片所能記錄的雖然只有聲音 然 而聲音 亦即 唱腔 正是戲曲藝術的核心之一

More information

The Development of Color Constancy and Calibration System

The Development of Color Constancy and Calibration System The Development of Color Constancy and Calibration System The Development of Color Constancy and Calibration System LabVIEW CCD BMP ii Abstract The modern technologies develop more and more faster, and

More information

University of Science and Technology of China A dissertation for master s degree Research of e-learning style for public servants under the context of

University of Science and Technology of China A dissertation for master s degree Research of e-learning style for public servants under the context of 中 国 科 学 技 术 大 学 硕 士 学 位 论 文 新 媒 体 环 境 下 公 务 员 在 线 培 训 模 式 研 究 作 者 姓 名 : 学 科 专 业 : 导 师 姓 名 : 完 成 时 间 : 潘 琳 数 字 媒 体 周 荣 庭 教 授 二 一 二 年 五 月 University of Science and Technology of China A dissertation for

More information

Microsoft Word - 論文封面-980103修.doc

Microsoft Word - 論文封面-980103修.doc 淡 江 大 學 中 國 文 學 學 系 碩 士 在 職 專 班 碩 士 論 文 指 導 教 授 : 呂 正 惠 蘇 敏 逸 博 士 博 士 倚 天 屠 龍 記 愛 情 敘 事 之 研 究 研 究 生 : 陳 麗 淑 撰 中 華 民 國 98 年 1 月 淡 江 大 學 研 究 生 中 文 論 文 提 要 論 文 名 稱 : 倚 天 屠 龍 記 愛 情 敘 事 之 研 究 頁 數 :128 校 系 (

More information

BIBLID 0254-4466(2000)18: pp. 231-260 18 89 12 ** 1992 1987 * ** 231 232 1991 1998 1958 1995 1998 1994 1989 233 1987 196 1989 82-83 234 1992 1994 1 2 1994 60 1 1. 2. 2 235 1989 37 3 4 1992 74 3 4 236 1-2

More information

Preface This guide is intended to standardize the use of the WeChat brand and ensure the brand's integrity and consistency. The guide applies to all d

Preface This guide is intended to standardize the use of the WeChat brand and ensure the brand's integrity and consistency. The guide applies to all d WeChat Search Visual Identity Guidelines WEDESIGN 2018. 04 Preface This guide is intended to standardize the use of the WeChat brand and ensure the brand's integrity and consistency. The guide applies

More information

hks298cover&back

hks298cover&back 2957 6364 2377 3300 2302 1087 www.scout.org.hk scoutcraft@scout.org.hk 2675 0011 5,500 Service and Scouting Recently, I had an opportunity to learn more about current state of service in Hong Kong

More information

~ ~ ~

~ ~ ~ 33 4 2014 467 478 Studies in the History of Natural Sciences Vol. 33 No. 4 2014 030006 20 20 N092 O6-092 A 1000-1224 2014 04-0467-12 200 13 Roger Bacon 1214 ~ 1292 14 Berthold Schwarz 20 Luther Carrington

More information

中 國 學 研 究 期 刊 泰 國 農 業 大 學 บ นทอนเช นก น และส งผลก บการด ดแปลงจากวรรณกรรมมาเป นบทภาพยนตร และบทละคร โทรท ศน ด วยเช นก น จากการเคารพวรรณกรรมต นฉบ บเป นหล

中 國 學 研 究 期 刊 泰 國 農 業 大 學 บ นทอนเช นก น และส งผลก บการด ดแปลงจากวรรณกรรมมาเป นบทภาพยนตร และบทละคร โทรท ศน ด วยเช นก น จากการเคารพวรรณกรรมต นฉบ บเป นหล วารสารจ นศ กษา มหาว ทยาล ยเกษตรศาสตร การเล อกสรรของย คสม ยท แตกต างก น โดยว เคราะห การด ดแปลง บทละครโทรท ศน หร อบทภาพยนต จากผลงานคลาสส กวรรณกรรม สม ยใหม ของจ น The Choice of Times Film Adaptation of Chinese

More information

Microsoft Word - 11月電子報1130.doc

Microsoft Word - 11月電子報1130.doc 發 行 人 : 楊 進 成 出 刊 日 期 2008 年 12 月 1 日, 第 38 期 第 1 頁 / 共 16 頁 封 面 圖 話 來 來 來, 來 葳 格 ; 玩 玩 玩, 玩 數 學 在 11 月 17 到 21 日 這 5 天 裡 每 天 一 個 題 目, 孩 子 們 依 據 不 同 年 段, 尋 找 屬 於 自 己 的 解 答, 這 些 數 學 題 目 和 校 園 情 境 緊 緊 結

More information

數學導論 學數學 前言 學 學 數學 學 數學. 學數學 論. 學,. (Logic), (Set) 數 (Function)., 學 論. 論 學 數學.,,.,.,., 論,.,. v Chapter 1 Basic Logic 學 數學 學 言., logic. 學 學,, 學., 學 數學. 數學 論 statement. 2 > 0 statement, 3 < 2 statement

More information

C o n t e n t s...7... 15 1. Acceptance... 17 2. Allow Love... 19 3. Apologize... 21 4. Archangel Metatron... 23 5. Archangel Michael... 25 6. Ask for

C o n t e n t s...7... 15 1. Acceptance... 17 2. Allow Love... 19 3. Apologize... 21 4. Archangel Metatron... 23 5. Archangel Michael... 25 6. Ask for Doreen Virtue, Ph.D. Charles Virtue C o n t e n t s...7... 15 1. Acceptance... 17 2. Allow Love... 19 3. Apologize... 21 4. Archangel Metatron... 23 5. Archangel Michael... 25 6. Ask for a Sign... 27 7.

More information

南華大學數位論文

南華大學數位論文 Rebuilding The Golden Town Everyday Life and Space at Jin-gua-shi 1897-1987.. ABSTRACT Rebuilding The Golden Town Everyday Life and Space at Jin-gua-shi ABSTRACT This thesis focuses on the formation of

More information

ABSTRACT ABSTRACT Based on analyzing public corporation in foreign countries, this paper studies basic theories of public legal establishment, with our country s reality in the social transferring period

More information

從篤加有二「區」談當代平埔文化復振現相

從篤加有二「區」談當代平埔文化復振現相 從 篤 加 有 二 邱 談 族 群 正 名 運 動 從 篤 加 有 二 邱 談 族 群 正 名 運 動 陳 榮 輝 台 南 女 子 技 術 學 院 通 識 教 育 中 心 講 師 摘 要 本 文 從 篤 加 村 非 平 埔 族 裔 的 正 名 運 動, 探 討 篤 加 村 民 因 不 認 同 廟 後 區 ( 邱 ) 所 形 成 的 平 埔 族 裔 概 念, 從 地 理 變 遷 村 廟 沿 革 族 譜

More information

985 Journal of CUPL No.2 A Bimo nt hly Mar ch 2 0 1 0 ABSTRACTS Getting to the Root and Compromising China with the West: Rebuilding the Chinese Legal System 5 Yu Ronggen /Professor,

More information

马 大 华 人 文 学 与 文 化 学 刊 Journal of Chinese Literature and Culture 6 前 言 顾 城 曾 在 接 受 德 国 汉 学 家 顾 彬 及 张 穗 子 专 访 中, 将 其 诗 歌 创 作 分 为 四 个 时 期, 即 自 然 阶 段 文 化

马 大 华 人 文 学 与 文 化 学 刊 Journal of Chinese Literature and Culture 6 前 言 顾 城 曾 在 接 受 德 国 汉 学 家 顾 彬 及 张 穗 子 专 访 中, 将 其 诗 歌 创 作 分 为 四 个 时 期, 即 自 然 阶 段 文 化 5 顾 城 水 银 组 诗 的 水 意 象 解 读 内 容 摘 要 : 意 象 长 久 以 来 扮 演 着 沟 通 人 与 物 之 间 的 桥 梁 在 顾 城 的 诗 歌 中, 意 象 更 发 挥 了 回 归 到 本 身 及 本 质 上 的 功 用 本 文 旨 在 探 讨 顾 城 组 诗 水 银 里 意 象 所 拼 凑 出 来 的 有 关 复 归 本 源 / 自 然 的 命 题 在 顾 城 笔 下,

More information

01何寄澎.doc

01何寄澎.doc 1 * ** * ** 2003 11 1-36 Imitation and the Formation and Interpretation of the Canon: Lu Chi s Nigushi Ho Chi-p eng Professor, Department of Chinese Literature, National Taiwan University. Hsu Ming-ch

More information

<4D6963726F736F667420576F7264202D20312E5FA473AEFCB867AED5AA605FBB50B04BCFC8AABAAFABB8DCACE3A8732E646F63>

<4D6963726F736F667420576F7264202D20312E5FA473AEFCB867AED5AA605FBB50B04BCFC8AABAAFABB8DCACE3A8732E646F63> 國 立 臺 南 大 學 人 文 與 社 會 研 究 學 報 第 44 卷 第 2 期 ( 民 國 99.10):1-24 山 海 經 校 注 與 袁 珂 的 神 話 研 究 鍾 佩 衿 國 立 政 治 大 學 中 文 研 究 所 碩 士 生 摘 要 作 為 中 國 神 話 研 究 的 重 要 學 者, 袁 珂 的 研 究 重 心 即 在 於 對 山 海 經 神 話 進 行 詮 釋 與 探 討 ; 研

More information

Abstract Since 1980 s, the Coca-Cola came into China and developed rapidly. From 1985 to now, the numbers of bottlers has increased from 3 to 23, and

Abstract Since 1980 s, the Coca-Cola came into China and developed rapidly. From 1985 to now, the numbers of bottlers has increased from 3 to 23, and Abstract Since 1980 s, the Coca-Cola came into China and developed rapidly. From 1985 to now, the numbers of bottlers has increased from 3 to 23, and increases ulteriorly. When the Coca-Cola company came

More information

问 她! 我 们 把 这 只 手 机 举 起 来 借 着 它 的 光 看 到 了 我 老 婆 正 睁 着 双 眼 你 在 干 什 么 我 问, 我 开 始 想 她 至 少 是 闭 着 眼 睛 在 yun 酿 睡 意 的 我 睡 不 着 她 很 无 辜 地 看 着 我 我 问 她 yun 酿 的 yu

问 她! 我 们 把 这 只 手 机 举 起 来 借 着 它 的 光 看 到 了 我 老 婆 正 睁 着 双 眼 你 在 干 什 么 我 问, 我 开 始 想 她 至 少 是 闭 着 眼 睛 在 yun 酿 睡 意 的 我 睡 不 着 她 很 无 辜 地 看 着 我 我 问 她 yun 酿 的 yu 果 皮 云 写 作 NO.6: 响 水 不 滚 滚 水 不 响 时 间 :2011 年 12 月 25 日 主 编 : 乌 青 作 者 : 秦 留, 新 a, 伊 文 达, 乌 青, 张 墩 墩, 娜 娜, 女 斑 马 王, 马 其 顿 荒 原, 尼 码, 萨 尔 卡, 傀 儡 尫 仔, 东 成, 二 天, 老 马 迷 途, 曾 骞, 郑 在, 柚 子, 以 下 简 称 刘 某, 大 棋, 张 维,

More information

< F5FB77CB6BCBD672028B0B6A46AABE4B751A874A643295F5FB8D5C5AA28A668ADB6292E706466>

< F5FB77CB6BCBD672028B0B6A46AABE4B751A874A643295F5FB8D5C5AA28A668ADB6292E706466> A A A A A i A A A A A A A ii Introduction to the Chinese Editions of Great Ideas Penguin s Great Ideas series began publication in 2004. A somewhat smaller list is published in the USA and a related, even

More information

致 谢 本 论 文 能 得 以 完 成, 首 先 要 感 谢 我 的 导 师 胡 曙 中 教 授 正 是 他 的 悉 心 指 导 和 关 怀 下, 我 才 能 够 最 终 选 定 了 研 究 方 向, 确 定 了 论 文 题 目, 并 逐 步 深 化 了 对 研 究 课 题 的 认 识, 从 而 一

致 谢 本 论 文 能 得 以 完 成, 首 先 要 感 谢 我 的 导 师 胡 曙 中 教 授 正 是 他 的 悉 心 指 导 和 关 怀 下, 我 才 能 够 最 终 选 定 了 研 究 方 向, 确 定 了 论 文 题 目, 并 逐 步 深 化 了 对 研 究 课 题 的 认 识, 从 而 一 中 美 国 际 新 闻 的 叙 事 学 比 较 分 析 以 英 伊 水 兵 事 件 为 例 A Comparative Analysis on Narration of Sino-US International News Case Study:UK-Iran Marine Issue 姓 名 : 李 英 专 业 : 新 闻 学 学 号 : 05390 指 导 老 师 : 胡 曙 中 教 授 上 海

More information

Chinese Journal of Applied Probability and Statistics Vol.25 No.4 Aug (,, ;,, ) (,, ) 应用概率统计 版权所有, Zhang (2002). λ q(t)

Chinese Journal of Applied Probability and Statistics Vol.25 No.4 Aug (,, ;,, ) (,, ) 应用概率统计 版权所有, Zhang (2002). λ q(t) 2009 8 Chinese Journal of Applied Probability and Statistics Vol.25 No.4 Aug. 2009,, 541004;,, 100124),, 100190), Zhang 2002). λ qt), Kolmogorov-Smirov, Berk and Jones 1979). λ qt).,,, λ qt),. λ qt) 1,.

More information

124 第十三期 Conflicts in the Takeover of the Land in Taiwan after the Sino-Japanese War A Case in the Change of the Japanese Names of the Taiwanese Peopl

124 第十三期 Conflicts in the Takeover of the Land in Taiwan after the Sino-Japanese War A Case in the Change of the Japanese Names of the Taiwanese Peopl 123 戰後初期臺灣土地接收的糾紛 以更改日式姓名的臺人遭遇為例 124 第十三期 Conflicts in the Takeover of the Land in Taiwan after the Sino-Japanese War A Case in the Change of the Japanese Names of the Taiwanese People Abstract By Ho Fung-jiao

More information

<4D6963726F736F667420576F7264202D20BCFAA755AAA92DABC8AE61AAE1A5ACB2A3B77EB56FAE69A4A7ACE3A873A147A548B8EAB7BDB0F2C2A6AABAC65BC2492E646F63>

<4D6963726F736F667420576F7264202D20BCFAA755AAA92DABC8AE61AAE1A5ACB2A3B77EB56FAE69A4A7ACE3A873A147A548B8EAB7BDB0F2C2A6AABAC65BC2492E646F63> 國 立 中 央 大 學 客 家 政 治 經 濟 研 究 所 碩 士 班 碩 士 論 文 客 家 花 布 產 業 發 展 之 研 究 : 以 資 源 基 礎 的 觀 點 研 究 生 : 李 怡 萱 指 導 教 授 : 周 錦 宏 博 士 中 華 民 國 九 十 七 年 二 月 本 論 文 獲 行 政 院 客 家 委 員 會 98 年 度 客 家 研 究 優 良 博 碩 士 論 文 獎 助 行 政 院

More information

Abstract There arouses a fever pursuing the position of being a civil servant in China recently and the phenomenon of thousands of people running to a

Abstract There arouses a fever pursuing the position of being a civil servant in China recently and the phenomenon of thousands of people running to a Abstract There arouses a fever pursuing the position of being a civil servant in China recently and the phenomenon of thousands of people running to attend the entrance examination of civil servant is

More information

從詩歌的鑒賞談生命價值的建構

從詩歌的鑒賞談生命價值的建構 Viktor E. Frankl (logotherapy) (will-to-meaning) (creative values) Ture (Good) (Beauty) (experiential values) (attitudinal values) 1 2 (logotherapy) (biological) (2) (psychological) (3) (noölogical) (4)

More information

601988 2010 040 113001 2010 8 26 2010 8 12 2010 8 26 15 15 2010 15 0 0 15 0 0 6035 20022007 20012002 19992001 200720081974 1999 2010 20082008 2000 197

601988 2010 040 113001 2010 8 26 2010 8 12 2010 8 26 15 15 2010 15 0 0 15 0 0 6035 20022007 20012002 19992001 200720081974 1999 2010 20082008 2000 197 BANK OF CHINA LIMITED 3988 2010 8 26 ** ** *** # Alberto TOGNI # # # * # 1 601988 2010 040 113001 2010 8 26 2010 8 12 2010 8 26 15 15 2010 15 0 0 15 0 0 6035 20022007 20012002 19992001 200720081974 1999

More information

謝 辭 還 記 得 在 宜 蘭 迎 新 那 晚, 眾 人 在 天 燈 上 寫 下 自 己 的 心 願, 將 天 燈 點 燃 後 放 開, 任 其 冉 冉 升 空 天 燈 成 功 上 升 了, 願 望 就 會 實 現 了 嗎? 看 來 答 案 是 肯 定 的, 因 為 我 終 於 順 利 完 成 論

謝 辭 還 記 得 在 宜 蘭 迎 新 那 晚, 眾 人 在 天 燈 上 寫 下 自 己 的 心 願, 將 天 燈 點 燃 後 放 開, 任 其 冉 冉 升 空 天 燈 成 功 上 升 了, 願 望 就 會 實 現 了 嗎? 看 來 答 案 是 肯 定 的, 因 為 我 終 於 順 利 完 成 論 東 吳 大 學 政 治 學 系 碩 士 論 文 指 導 教 授 : 陳 俊 宏 博 士 平 等 與 差 異 之 辯 證 : 社 會 秩 序 維 護 法 中 罰 娼 不 罰 嫖 條 款 修 法 爭 議 之 研 究 The Dialectics of the Equality and the Differences: The Controversial Amendment of the prohibition

More information

03

03 BIBLID 0254-4466(2002)20:2 pp. 57-80 20 2 91 12 vs. 1684-? * 57 58 20 2 1 2 3 4 5 transmission transformation 6 Whiggish interpretation 1 2000 8 559-563 539-558 1993 4 64-67 16 4 1995 3-7 2 1978 3 4 HPM

More information

P

P 100871 I0-03 A 1671-7511 2011 04-0072 - 11 6 18 1 2 3 4 2010-01 - 04 1 2 3 4 72 1 20 2 1 P309 310 1 2 73 1 3 2 1933 1 2 3 74 13 1976 7 2 1 2 P281 1929 1930 1935 1937 1948 1 2 1933 3 25 11 1998 5 ~ 1999

More information

untitled

untitled LBS Research and Application of Location Information Management Technology in LBS TP319 10290 UDC LBS Research and Application of Location Information Management Technology in LBS , LBS PDA LBS

More information

A-錢穆宗教觀-171

A-錢穆宗教觀-171 台 南 應 用 科 大 學 報 第 32 期 人 文 管 理 類 頁 171-186 中 華 民 國 102 年 10 月 錢 穆 宗 教 觀 析 論 以 文 化 與 教 育 為 觀 察 核 心 梁 淑 芳 國 立 體 育 大 學 通 識 教 育 中 心 助 理 教 授 摘 要 國 學 大 師 錢 穆, 可 謂 一 代 通 儒 本 文 以 其 文 化 與 教 育 為 主, 輔 以 錢 穆 的 其 餘

More information

Microsoft Word - 刘藤升答辩修改论文.doc

Microsoft Word - 刘藤升答辩修改论文.doc 武 汉 体 育 学 院 硕 士 学 位 论 文 ( 全 日 制 硕 士 ) 社 会 需 求 视 角 下 武 汉 体 院 乒 乓 球 硕 士 研 究 生 就 业 状 况 研 究 研 究 生 : 刘 藤 升 导 师 : 滕 守 刚 副 教 授 专 业 : 体 育 教 育 训 练 学 研 究 方 向 : 乒 乓 球 教 学 训 练 理 论 与 方 法 2015 年 5 月 分 类 号 : G8 学 校 代

More information

<453A5CB1BED0A3CBB6CABFC2DBCEC45C3037BCB6CBB6CABFC2DBCEC4A3A8504446A3A95C32303130BDECC8CBCEC4D1A7D4BAB1CFD2B5C2DBCEC45CC3F1CBD7D1A75CBAFAB1FEC4EAB1CFD2B5C2DBCEC4A3A8CEDED2B3C3BCA3A92E646F63>

<453A5CB1BED0A3CBB6CABFC2DBCEC45C3037BCB6CBB6CABFC2DBCEC4A3A8504446A3A95C32303130BDECC8CBCEC4D1A7D4BAB1CFD2B5C2DBCEC45CC3F1CBD7D1A75CBAFAB1FEC4EAB1CFD2B5C2DBCEC4A3A8CEDED2B3C3BCA3A92E646F63> 分 类 号 : K890 学 号 :_07105822006_ UDC: 300 密 级 :_ 公 开 硕 士 学 位 论 文 温 州 模 式 的 民 俗 文 化 语 境 研 究 A STUDAY OF THE BACKGROUND OF FOLK CULYURE IN WENZHOU MODEL 作 者 姓 名 : 学 科 专 业 : 研 究 方 向 : 指 导 教 师 : 完 成 日 期 : 胡

More information

* RRB *

* RRB * *9000000000RRB0010040* *9000000000RRB0020040* *9000000000RRB0030040* *9000000000RRB0040040* *9000000000RRC0010050* *9000000000RRC0020050* *9000000000RRC0030050* *9000000000RRC0040050* *9000000000RRC0050050*

More information

<4D6963726F736F667420576F7264202D2035B171AB73B6CBA8ECAB73A6D3A4A3B6CBA158B3AFA46CA9F9BB50B169A445C4D6AABAB750B94AB8D6B9EFA4F1ACE3A873>

<4D6963726F736F667420576F7264202D2035B171AB73B6CBA8ECAB73A6D3A4A3B6CBA158B3AFA46CA9F9BB50B169A445C4D6AABAB750B94AB8D6B9EFA4F1ACE3A873> 中 正 漢 學 研 究 2012 年 第 一 期 ( 總 第 十 九 期 ) 2012 年 6 月 頁 111~134 國 立 中 正 大 學 中 國 文 學 系 111 從 哀 傷 到 哀 而 不 傷 : 陳 子 昂 與 張 九 齡 的 感 遇 詩 對 比 研 究 * 丁 涵 摘 要 在 中 國 古 典 文 學 語 境 中, 一 個 主 題 的 奠 立 往 往 需 要 歷 時 彌 久, 而 這 本

More information

影響新產品開發成效之造型要素探討

影響新產品開發成效之造型要素探討 異 行 車 例 A Study on the Product Forms Recognition Difference between Designer and Consumer --- Electrical Bicycle as Example. 行 車 省 力 力 綠 老 女 行 車 行 車 了 不 了 行 行 車 行 車 不 行 車 異 行 車 車 車 行 行 異 數 量 I 類 行 異 異

More information

9 21-40 2004 12 * * 22 9 1 2 3 1 1992 2 1960 2 3 1984 8 87 23 4 5 1697 AD 1779 6 7 8 9 10 11 12 4 1977 109-112 5 87 41993 13-38 6 614 7 8 632 9 1974 8 10 631 11 12 632 9 24 13 14 13 1990 14 25 15 16 15

More information

BIBLID 0254-4466(2001)19:1 pp. 249-276 19 1 90 6 ** * ** 88 I 2000 8 249 250 19 1 251 1873-1929 1900 1 1902 1 35 1900 1960 7-12 252 19 1 2 3 2 1900 1902 3 2000 129-197 253 4 5 6 4 1902 1962 103 5 Joseph

More information

ABP

ABP ABP 2016 319 1 ABP A. D. Aleksandrov,I. Y. Bakelman,C. Pucci 1 2 ABP 3 ABP 4 5 2 Ω R n : bounded C 0 = C 0 (n) > 0 such that u f in Ω (classical subsolution) max Ω u max u + C 0diam(Ω) 2 f + L Ω (Ω) 3

More information

Microsoft Word - Final Exam Review Packet.docx

Microsoft Word - Final Exam Review Packet.docx Do you know these words?... 3.1 3.5 Can you do the following?... Ask for and say the date. Use the adverbial of time correctly. Use Use to ask a tag question. Form a yes/no question with the verb / not

More information

地質調査研究報告/Bulletin of the Geological Survey of Japan

地質調査研究報告/Bulletin of the Geological Survey of Japan Shigeru Suto, Takayuki Inomata, Hisashi Sasaki and Sakae Mukoyama (2007) Data base of the volcanic ash fall distribution map of Japan. Bull. Geol. Surv. Japan, vol. 58(9/10), p.261-321, 8 figs, 2 tables,

More information

096STUT DOC

096STUT DOC i YouTube was established in 2005 until now only more than 3 years. Although it was established just more than 3 years, it has already become the one of multitudinous video shares website that most people

More information

Chn 116 Neh.d.01.nis

Chn 116 Neh.d.01.nis 31 尼 希 米 书 尼 希 米 的 祷 告 以 下 是 哈 迦 利 亚 的 儿 子 尼 希 米 所 1 说 的 话 亚 达 薛 西 王 朝 二 十 年 基 斯 流 月 *, 我 住 在 京 城 书 珊 城 里 2 我 的 兄 弟 哈 拿 尼 和 其 他 一 些 人 从 犹 大 来 到 书 珊 城 我 向 他 们 打 听 那 些 劫 后 幸 存 的 犹 太 人 家 族 和 耶 路 撒 冷 的 情 形

More information

Microsoft Word - 24.doc

Microsoft Word - 24.doc 水 陸 畢 陳 晚 明 飲 食 風 尚 初 探 蕭 慧 媛 桃 園 創 新 技 術 學 院 觀 光 與 休 閒 事 業 管 理 系 摘 要 飲 食 是 人 類 維 持 與 發 展 生 命 的 基 礎 之 一, 飲 食 風 尚 會 隨 著 社 會 地 位 物 質 條 件 以 及 人 為 因 素 轉 移, 不 同 階 層 的 飲 食 方 式, 往 往 標 誌 著 他 們 的 社 會 身 分, 甚 至 反

More information

天 主 教 輔 仁 大 學 社 會 學 系 學 士 論 文 小 別 勝 新 婚? 久 別 要 離 婚? 影 響 遠 距 家 庭 婚 姻 感 情 因 素 之 探 討 Separate marital relations are getting better or getting worse? -Exp

天 主 教 輔 仁 大 學 社 會 學 系 學 士 論 文 小 別 勝 新 婚? 久 別 要 離 婚? 影 響 遠 距 家 庭 婚 姻 感 情 因 素 之 探 討 Separate marital relations are getting better or getting worse? -Exp 天 主 教 輔 仁 大 學 社 會 學 系 學 士 論 文 小 別 勝 新 婚? 久 別 要 離 婚? 影 響 遠 距 家 庭 婚 姻 感 情 因 素 之 探 討 Separate marital relations are getting better or getting worse? -Explore the impact of emotional factors couples do not

More information

高中英文科教師甄試心得

高中英文科教師甄試心得 高 中 英 文 科 教 師 甄 試 心 得 英 語 學 系 碩 士 班 林 俊 呈 高 雄 市 立 高 雄 高 級 中 學 今 年 第 一 次 參 加 教 師 甄 試, 能 夠 在 尚 未 服 兵 役 前 便 考 上 高 雄 市 立 高 雄 高 級 中 學 專 任 教 師, 自 己 覺 得 很 意 外, 也 很 幸 運 考 上 後 不 久 在 與 雄 中 校 長 的 會 談 中, 校 長 的 一 句

More information

Microsoft Word - ChineseSATII .doc

Microsoft Word - ChineseSATII .doc 中 文 SAT II 冯 瑶 一 什 么 是 SAT II 中 文 (SAT Subject Test in Chinese with Listening)? SAT Subject Test 是 美 国 大 学 理 事 会 (College Board) 为 美 国 高 中 生 举 办 的 全 国 性 专 科 标 准 测 试 考 生 的 成 绩 是 美 国 大 学 录 取 新 生 的 重 要 依

More information

Introduction to Hamilton-Jacobi Equations and Periodic Homogenization

Introduction to Hamilton-Jacobi Equations  and Periodic Homogenization Introduction to Hamilton-Jacobi Equations and Periodic Yu-Yu Liu NCKU Math August 22, 2012 Yu-Yu Liu (NCKU Math) H-J equation and August 22, 2012 1 / 15 H-J equations H-J equations A Hamilton-Jacobi equation

More information

<4D6963726F736F667420576F7264202D2031322D312DC2B2B4C2AB47A16DC5AAAED1B0F3B5AAB0DDA144A7B5B867A16EB2A4B1B4A277A548AED1A4A4BEC7A5CDB0DDC344ACB0A8D2>

<4D6963726F736F667420576F7264202D2031322D312DC2B2B4C2AB47A16DC5AAAED1B0F3B5AAB0DDA144A7B5B867A16EB2A4B1B4A277A548AED1A4A4BEC7A5CDB0DDC344ACB0A8D2> 弘 光 人 文 社 會 學 報 第 12 期 簡 朝 亮 讀 書 堂 答 問. 孝 經 略 探 以 書 中 學 生 問 題 為 例 趙 詠 寬 彰 化 師 範 大 學 國 文 學 系 博 士 班 研 究 生 摘 要 孝 經 是 十 三 經 中 字 數 最 少 的 經 典, 然 實 踐 性 高, 受 歷 來 帝 王 重 視 但 在 清 末 民 初, 傳 統 思 維 受 到 挑 戰, 被 視 為 維 護

More information

南華大學數位論文

南華大學數位論文 南華大學 碩士論文 中華民國九十五年六月十四日 Elfin Excel I II III ABSTRACT Since Ming Hwa Yuan Taiwanese Opera Company started to cooperate with the Chinese orchestra, the problem of how the participation of Chinese music

More information

A study on the Fire Safety of Interior Finishes: Residential Buildings in Kaohsiung City taken as Examples between the interior design of safety and skill tests of Scholastic. A Thesis Submitted to Institute

More information

穨6街舞對抗中正紀念堂_林伯勳張金鶚_.PDF

穨6街舞對抗中正紀念堂_林伯勳張金鶚_.PDF ( ) 115 115140 Journal of City and Planning(2002) Vol.29, No.1, pp.115140 90 10 26 91 05 20 2 3 --- ( ) 1. 2. mag.ryan@msa.hinet.net 3. jachang@nccu.edu.tw 1018-1067/02 2002 Chinese Institute of Urban

More information