文献

J-GLOBAL ID：202002270466014460   整理番号：20A0018781

集合切断型高次帰納型の構築【JST・京大機械翻訳】

The Construction of Set-Truncated Higher Inductive Types

著者 (2件)： van der Weide Niels (Institute for Computation and Information Sciences, Radboud Universiteit Nijmegen, the Netherlands) ,  Geuvers Herman (Institute for Computation and Information Sciences, Radboud Universiteit Nijmegen, the Netherlands)
資料名： Electronic Notes in Theoretical Computer Science  (Electronic Notes in Theoretical Computer Science)
巻： 347  ページ： 261-280  発行年： 2019年 
JST資料番号： W2857A  ISSN： 1571-0661  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： オランダ (NLD)  言語： 英語 (EN)

抄録/ポイント： 著者らは,quotientsと命題の切断から,最終的にセットされたより高い誘導型(ヒット)を構築する。そのために,最初に,Basoldらによるスキーマの修正として署名を定義し,それらが集合とセトイドの両方における代数の非等価なカテゴリをもたらすことを示した。ヒットを解釈するために,著者らは初期代数意味論のよく知られた方法を使用した。要求される代数は,代数のレベルに対する商の付加を持ち上げることによって得られ,そして,セトイドにおけるヒットのDybjerとMoeneclaeyの解釈を適応させることによって得られる。この構築から,ヒットの等式型が自由に生成され,ヒットが独特であると結論した。結果はUniMathライブラリで定式化した。Copyright 2020 Elsevier B.V., Amsterdam. All rights reserved. Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 命題 ,  意味論 ,  データ構造 ,  定式化 ,  代数学 ,  *帰納推論

著者キーワード (6件)： 高次誘導型 ,  ホモトピー型理論 ,  カテゴリー理論 ,  セトイド ,  直感型理論 ,  Coq

分類 (3件)： 計算理論  (JB02000A) ,  計算機システム開発  (JD02010R) ,  数理言語学  (JB05000V)

タイトルに関連する用語 (3件)： 集合 ,  帰納 ,  構築