{"id":"W3181469359","doi":"10.48550/arxiv.2107.04859","title":"Approximate Normalization and Eager Equality Checking for Gradual Inductive Families","year":2021,"lang":"en","type":"preprint","venue":"arXiv (Cornell University)","topic":"Logic, programming, and type systems","field":"Computer Science","cited_by":0,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of British Columbia","funders":"","keywords":"Computer science; Programming language; Normalization (sociology); Decidability; Type inference; Compiler; Compile time; Type theory; Theoretical computer science; Mathematical proof; Dependent type; Type (biology); Data type; Artificial intelligence; Mathematics; Inference","routes":{"ca_aff":true,"ca_fund":false,"ca_venue":false,"about_ca":false,"invisible_to_affiliation_only":false},"retraction":null,"screen":null,"direct_labels":[],"prediction":{"model_version":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.006371179,0.0009254894,0.00106602,0.001862411,0.001617751,0.003290123,0.004034189,0.001468964,0.004799531],"category_scores_gemma":[0.02954668,0.001262688,0.003854471,0.001273787,0.005180222,0.01011994,0.006721159,0.004810426,0.001321381],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.003523841,"about_ca_system_score_gemma":0.003308878,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.003813757,"about_ca_topic_score_gemma":0.004512801,"domain_scores_codex":[0.9888967,0.00252399,0.000889776,0.002546519,0.004014306,0.001128596],"domain_scores_gemma":[0.9840014,0.00880003,0.001122764,0.003388374,0.002277345,0.0004100639],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"theoretical_or_conceptual","study_design_scores_codex":[0.0003618351,0.0001372296,0.005759875,0.0003569021,0.0001281768,0.0005611437,0.001297182,0.05775639,0.01841921,0.8189561,0.003333574,0.09293234],"study_design_scores_gemma":[0.00005934021,0.0000985494,0.0005756727,0.0001224677,0.0001252089,0.0002938886,0.0001549315,0.2380121,0.02718044,0.7191612,0.01410598,0.0001102893],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.03078869,0.0002051918,0.9590918,0.0005111751,0.0001128116,0.0001079898,0.0002358151,0.003462875,0.005483643],"genre_scores_gemma":[0.4644436,0.0002331576,0.5223293,0.0009361155,0.0001817165,0.0003719468,0.0006906476,0.001728724,0.009084908],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.006371179,"threshold_uncertainty_score":0.03369445,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.1161746181982713,"score_gpt":0.2177191901240443,"score_spread":0.1015445719257731,"validation_status":"score_only:v0-immature-baseline","note":"Baseline scores from an immature model (maturity gate not passed). Scores rank; they never assert a category."}}