Pith. Sign in

RECORD

Positive Inductive-Recursive Definitions

PaperPDF from arXiv

data files

Paper breakdownThe authors' claims, conditions and measurements, as JSON Signed receiptProof this review has not been altered
X Bluesky LinkedIn Reddit Hacker News
Neil Ghani (University of Strathclyde), Fredrik Nordvall Forsberg (University of Strathclyde), Lorenzo Malatesta (University of Strathclyde)

Logic in Computer Science · Submitted 19 Feb 2015

abstract compiled · 2026-09-23 · no language-model review

The authors' main claim A new theory of data types which allows for the definition of types as initial algebras of certain functors Fam(C) -> Fam(C) is presented.

how it is stated · asserted 1.00 read the record →

Comment (0) Read on arXiv ↗
Cite ▾
arXiv ID1502.05561 (version 2)
Pith IDUD2S2STX, Pith's permanent record of this paper and its review
CitationFredrik Nordvall Forsberg (University of Strathclyde), Lorenzo Malatesta (University of Strathclyde), Neil Ghani (University of Strathclyde). "Positive Inductive-Recursive Definitions." arXiv:1502.05561 (2015). https://pith.science/paper/UD2S2STX
Claim paper

The compiled record

The paper's own sentences, arranged. Each label is drawn from a closed vocabulary; the number beside it is the probability the classifier gave that label. Numbers in the tables are the authors', checked by code. No sentence in this record was written by a model.

Open the compiled record

Compiled by classifier-1.13-20260917 via OpenRouter, question bank abstract-p1-20260923, 2026-09-23: 1 request, 5,121 input tokens, $0.0002 reported.

What the abstract itself states, as probabilities: claims first 0.10 · states limitation 0.11 · human participants 0.01 · controlled comparison 0.03 · randomized assignment 0.01 · states quantitative result 0.03 · compares with prior results 0.96 · mentions code or data availability 0.02.

The abstract, sentence by sentence

arXiv listing abstract v2. Results and the main claim are underlined; .

A new theory of data types which allows for the definition of types as initial algebras of certain functors Fam(C) -> Fam(C) is presented. This theory, which we call positive inductive-recursive definitions, is a generalisation of Dybjer and Setzer's theory of inductive-recursive definitions within which C had to be discrete -- our work can therefore be seen as lifting this restriction. This is a substantial endeavour as we need to not only introduce a type of codes for such data types (as in Dybjer and Setzer's work), but also a type of morphisms between such codes (which was not needed in Dybjer and Setzer's development). We show how these codes are interpreted as functors on Fam(C) and how these morphisms of codes are interpreted as natural transformations between such functors. We then give an application of positive inductive-recursive definitions to the theory of nested data types and we give concrete examples of recursive functions defined on universes by using their elimination principle. Finally we justify the existence of positive inductive-recursive definitions by adapting Dybjer and Setzer's set-theoretic model to our setting.

background contribution method result interpretation main claim

What the classifier reports for each sentence. The number is the probability it gave the label.
#sentencerolethe authors' own workstates the main conclusionstrength
s0 A new theory of data types which allows for the definition of types as initial algebras of certain functors Fam(C) -> Fam(C) is presented. contribution 1.00 0.90 0.31 asserted 1.00
s1 This theory, which we call positive inductive-recursive definitions, is a generalisation of Dybjer and Setzer's theory of inductive-recursive definitions within which C had to be discrete -- our work can therefore be seen as lifting this restriction. contribution 0.63 0.61 0.19 asserted 1.00
s2 This is a substantial endeavour as we need to not only introduce a type of codes for such data types (as in Dybjer and Setzer's work), but also a type of morphisms between such codes (which was not needed in Dybjer and Setzer's development). contribution 0.67 0.85 0.06 asserted 1.00
s3 We show how these codes are interpreted as functors on Fam(C) and how these morphisms of codes are interpreted as natural transformations between such functors. method 0.60 0.94 0.08 asserted 1.00
s4 We then give an application of positive inductive-recursive definitions to the theory of nested data types and we give concrete examples of recursive functions defined on universes by using their elimination principle. contribution 0.95 0.95 0.11 asserted 1.00
s5 Finally we justify the existence of positive inductive-recursive definitions by adapting Dybjer and Setzer's set-theoretic model to our setting. contribution 0.52 0.93 0.31 asserted 1.00

What kind of paper the classifier reports this is: theoretical result 0.80 · evidence from proof or derivation 1.00.

What was examined, and what was not

sources read
  • arXiv listing abstract v2
not examined
  • full text
  • figures and tables
  • references and citing sentences
  • relations to other papers
levels run
  • P abstract
not run
  • S sections
  • T body sentences
  • C citations
  • R cross-paper relations

Every quoted sentence on this record is the authors'. Every label is from Pith's closed vocabulary, with the probability shown beside it. Every number in the measurements table is the authors', checked by code. Record as JSON

The paper
Original abstract

A new theory of data types which allows for the definition of types as initial algebras of certain functors Fam(C) -> Fam(C) is presented. This theory, which we call positive inductive-recursive definitions, is a generalisation of Dybjer and Setzer's theory of inductive-recursive definitions within which C had to be discrete -- our work can therefore be seen as lifting this restriction. This is a substantial endeavour as we need to not only introduce a type of codes for such data types (as in Dybjer and Setzer's work), but also a type of morphisms between such codes (which was not needed in Dybjer and Setzer's development). We show how these codes are interpreted as functors on Fam(C) and how these morphisms of codes are interpreted as natural transformations between such functors. We then give an application of positive inductive-recursive definitions to the theory of nested data types and we give concrete examples of recursive functions defined on universes by using their elimination principle. Finally we justify the existence of positive inductive-recursive definitions by adapting Dybjer and Setzer's set-theoretic model to our setting.

Human review

How Pith checks papers → · Full audit of this paper →

Discussion

Know something about this paper? Leave a comment, or highlight any passage above to comment on it.