This paper presents a method to define a set of mutuaJly recursive inductive types, and develops a higherorder unilication algorithm for Anz extended with inductive types. The algorithm is an extension of Eiliott'...This paper presents a method to define a set of mutuaJly recursive inductive types, and develops a higherorder unilication algorithm for Anz extended with inductive types. The algorithm is an extension of Eiliott's algoritbJn for λ∑.The notation of normal forms plays a vital role in higher-order unification.The weak head normal forms in the extended troe theory is defined to reveal the ultimate 'top level structures' of the fully normalized terms and types. Unification transformation rules are designed to deal with inductive types, a recursive operator and its reduction rule. The algoritlun can construct recuxsive functions automatically.展开更多
The goal of this contribution is to explain the analogy between combinatorial Dyson-Schwinger equations and inductive data types to a readership of mathematical physicists. The connection relies on an interpretation o...The goal of this contribution is to explain the analogy between combinatorial Dyson-Schwinger equations and inductive data types to a readership of mathematical physicists. The connection relies on an interpretation of combinatorial Dyson-Schwinger equations as fixpoint equations for polynomial functors （established elsewhere by the author, and summarised here）, combined with the now-classical fact that polynomial functors provide semantics for inductive types. The paper is expository, and comprises also a brief introduction to type theory.展开更多
As a subtask of open domain event extraction(ODEE),new event type induction aims to discover a set of unseen event types from a given corpus.Existing methods mostly adopt semi-supervised or unsupervised learning to ac...As a subtask of open domain event extraction(ODEE),new event type induction aims to discover a set of unseen event types from a given corpus.Existing methods mostly adopt semi-supervised or unsupervised learning to achieve the goal,which uses complex and different objective functions for labeled and unlabeled data respectively.In order to unify and simplify objective functions,a reliable pseudo-labeling prediction(RPP)framework for new event type induction was proposed.The framework introduces a double label reassignment(DLR)strategy for unlabeled data based on swap-prediction.DLR strategy can alleviate the model degeneration caused by swap-predication and further combine the real distribution over unseen event types to produce more reliable pseudo labels for unlabeled data.The generated reliable pseudo labels help the overall model be optimized by a unified and simple objective.Experiments show that RPP framework outperforms the state-of-the-art on the benchmark.展开更多
Inductive types can be formulated by incorporating the idea of initial T-algebra. The interpretation of an inductive type of this kind boils down to finding out the initial T-algebra defined by the inductive type. In ...Inductive types can be formulated by incorporating the idea of initial T-algebra. The interpretation of an inductive type of this kind boils down to finding out the initial T-algebra defined by the inductive type. In this paper the issue in the semantic domain of omega sets is examined. Based on the semantic results, a new class of inductive types, that of local inductive types, is proposed.展开更多
It is well known that impredicative type systems do not have set theoretical semantics. This paper takes a look at semantics of inductive types in impredicative type systems. A generalized inductive type is interprete...It is well known that impredicative type systems do not have set theoretical semantics. This paper takes a look at semantics of inductive types in impredicative type systems. A generalized inductive type is interpreted as an omega set generated by effectivizing a certain rule set. The result provides a semantic justification of inductive types in the calculus of constructions.展开更多
文摘This paper presents a method to define a set of mutuaJly recursive inductive types, and develops a higherorder unilication algorithm for Anz extended with inductive types. The algorithm is an extension of Eiliott's algoritbJn for λ∑.The notation of normal forms plays a vital role in higher-order unification.The weak head normal forms in the extended troe theory is defined to reveal the ultimate 'top level structures' of the fully normalized terms and types. Unification transformation rules are designed to deal with inductive types, a recursive operator and its reduction rule. The algoritlun can construct recuxsive functions automatically.
文摘The goal of this contribution is to explain the analogy between combinatorial Dyson-Schwinger equations and inductive data types to a readership of mathematical physicists. The connection relies on an interpretation of combinatorial Dyson-Schwinger equations as fixpoint equations for polynomial functors （established elsewhere by the author, and summarised here）, combined with the now-classical fact that polynomial functors provide semantics for inductive types. The paper is expository, and comprises also a brief introduction to type theory.
基金supported by the National Natural Science Foundation of China(62076031)。
文摘As a subtask of open domain event extraction(ODEE),new event type induction aims to discover a set of unseen event types from a given corpus.Existing methods mostly adopt semi-supervised or unsupervised learning to achieve the goal,which uses complex and different objective functions for labeled and unlabeled data respectively.In order to unify and simplify objective functions,a reliable pseudo-labeling prediction(RPP)framework for new event type induction was proposed.The framework introduces a double label reassignment(DLR)strategy for unlabeled data based on swap-prediction.DLR strategy can alleviate the model degeneration caused by swap-predication and further combine the real distribution over unseen event types to produce more reliable pseudo labels for unlabeled data.The generated reliable pseudo labels help the overall model be optimized by a unified and simple objective.Experiments show that RPP framework outperforms the state-of-the-art on the benchmark.
基金the National Natural Science Foundation of China (No.69973030). It is alsosupported by BASICS, Center of Basic Studies in Comp
文摘Inductive types can be formulated by incorporating the idea of initial T-algebra. The interpretation of an inductive type of this kind boils down to finding out the initial T-algebra defined by the inductive type. In this paper the issue in the semantic domain of omega sets is examined. Based on the semantic results, a new class of inductive types, that of local inductive types, is proposed.
基金This work is funded by the National Natural Science Foundation of China (No.69973030). It is alsosupported by BASICS, Center o
文摘It is well known that impredicative type systems do not have set theoretical semantics. This paper takes a look at semantics of inductive types in impredicative type systems. A generalized inductive type is interpreted as an omega set generated by effectivizing a certain rule set. The result provides a semantic justification of inductive types in the calculus of constructions.
