[ { "λδ-2B" + "(November 2019)" * }
{
[ [{ "validity" * }]
- { "@" "" "@" }
- { "+" "-" "*" }
- { "type assignment (terms)"
- "stratified higher validity (terms) removed"
+ { "" "@" "" "@" }
+ { "+" "+" "-" "*" }
+ { "iterated type assignment (terms)"
+ "type assignment (terms)"
+ "higher validity (terms) removed"
"primitive validity (terms)"
}
]
[ [{ "equivalences" * }]
- { "" "" "" "" }
- { "+" "+" "+" "-" }
- { "equivalence for full rt-reduction (terms)"
+ { "" "" "" "" "" "" "" }
+ { "+" "-" "+" "+" "+" "+" "-" }
+ { "derived rt-equivalence (terms)"
+ "primitive decomposed rt-equivalence (terms) removed"
"equivalence for whd rt-reduction (terms)"
- "equivalence for full rt-reduction (terms, referred lenvs, closures)"
- "syntactic equivalence (closures) removed"
+ "equivalence for full rt-reduction (terms, items, referred lenvs, referred closures)"
+ "equivalence up to exclusion binders (selected lenvs)"
+ "syntactic equivalence (items)"
+ "syntactic equivalence (selected closures) removed"
}
]
[ [{ "partial orders" * }]
- { "" }
- { "+" }
- { "switch in primitive order relations for closures to enable the exclusion binder"
+ { "" "" "" "" "" }
+ { "+" "+" "+" "+" "+" }
+ { "properties with inclusion (hereditarily free variables)"
+ "inclusion (hereditarily free variables)"
+ "inclusion (applicability)"
+ "switch in primitive order relations (closures) to enable the exclusion binder"
+ "simple weight (items, genvs)"
+ }
+ ]
+ [ [{ "reducibility" * }]
+ { "" "" "" }
+ { "+" "-" "*" }
+ { "compatibility relation for strong normalization (referred lenvs)"
+ "compatibility predicate for strong normalization (referred lenvs) removed"
+ "abatract Tait's candidates with 6 postulates"
}
]
[ [{ "normal form predicates" * }]
- { "" "" "" "" "" }
- { "-" "-" "-" "-" "-" }
- { "irreducible forms for full rt-reduction (terms) removed"
+ { "" "" "" "" "" "" "" "" "" "" }
+ { "+" "-" "+" "*" "+" "-" "-" "-" "-" "-" }
+ { "properties with evaluation"
+ "evaluation for full rt-reduction (terms) removed"
+ "whd evaluation for mixed rt-reduction (terms)"
+ "evaluation for mixed rt-reduction (terms)"
+ "whd normal form for mixed rt-reduction (terms)"
+ "irreducible forms for full rt-reduction (terms) removed"
"reducible forms for full rt-reduction (terms) removed"
"irreducible forms for reduction (terms) removed"
"reducible forms for reduction (terms) removed"
"abstract reducibility properties (items) removed"
}
]
+ [ [{ "reduction and type synthesis" * }]
+ { "" "" "@" "" "" "@" "" "" "@" "@" }
+ { "*" "*" "-" "+" "*" "+" "*" "+" "*" "+" }
+ { "counted iterated type synthesis (terms)"
+ "full rt-computation (terms, items, lenvs)"
+ "decomposed rt-computation (terms) removed"
+ "r-computation (items)"
+ "mixerd rt-computation (terms)"
+ "counted type synthesis (terms) with δ,s,l,e"
+ "full rt-transition (terms, items, lenvs, referred lenvs)"
+ "r-transition (items)"
+ "mixed rt-transition (terms)"
+ "primitive generic rt transition (terms) with typed β, δ, (correct) ζ, θ, ε"
+ }
+ ]
[ [{ "substitution" * }]
- { "" }
- { "-" }
- { "zero or more refs (terms) removed"
+ { "" "" }
+ { "-" "-" }
+ { "(restricted) zero or more selected refs (terms) removed"
+ "zero or more refs (terms) removed"
}
]
- [ [{ "relocation" * }]
- { "" "" "" "" }
- { "-" "*" "-" "*" }
- { "basic slicing (lenvs) removed"
+ [ [{ "degree" * }]
+ { "" "@" }
+ { "-" "-" }
+ { "refinement for degree (lenvs) removed"
+ "degree assignment (terms) removed"
+ }
+ ]
+ [ [{ "relocation and slicing" * }]
+ { "" "" "" "" "" "" "" }
+ { "-" "+" "-" "*" "-" "+" "*" }
+ { "look-up predicate (genvs) removed"
+ "properties with abstract relocation (terms/items)"
+ "basic slicing (lenvs) removed"
"primitive finite slicing (lenvs)"
- "basic relocation (lists of terms) removed"
+ "basic relocation (terms, lists of terms) removed"
+ "primitive finite relocation (items)"
"primitive finite relocation (terms, lists of terms)"
}
]
[ [{ "free varibles" * }]
- { "" }
- { "+" }
- { "union (referred lenvs) removed"
+ { "" "" }
+ { "+" "-" }
+ { "refinement for hereditarily free variables (lenvs)"
+ "union (referred lenvs) removed"
+ }
+ ]
+ [ [{ "helpers" * }]
+ { "" "" "" "" "" }
+ { "-" "+" "+" "-" "+" }
+ { "unfold (closures) removed"
+ "append (restricted closures) wrong on excluded entries"
+ "length (genvs)"
+ "refinement (selected lenvs) removed"
+ "abstract properties with append (lenvs)"
+ }
+ ]
+ [ [{ "extension" * }]
+ { "" "" "" "" "" }
+ { "+" "+" "+" "+" "+" }
+ { "properties with iterated extension (referred lenvs)"
+ "iterated for 3-relations (referred lenvs)"
+ "abstract properties with extension (selected lenvs)"
+ "for 3-relations (selected lenvs)"
+ "for 2-relations and 3-relations (items)"
}
]
[ [{ "syntax" * }]
- { "@" }
- { "+" }
- { "exclusion binder for lenvs"
+ { "@" "" }
+ { "+" "+" }
+ { "exclusion binder (lenvs)"
+ "bonding items (lenvs)"
+ }
+ ]
+ [ [{ "parameters" * }]
+ { "" "" "@" "" "" "@" }
+ { "+" "+" "+" "-" "+" "*" }
+ { "instances (applicability)"
+ "predicates (applicability)"
+ "abstract applicability condition"
+ "instances (sort hierarchy) removed"
+ "predicates (sort hierarchy) including strict monotonicity condition based on non-negative integers"
+ "abstract sort hierarchy without predicates"
}
]
[ [{ "ground" * }]
]
class "orange"
- [ { "λδ-2A" + "(October 2014)" * }
+ [ { "λδ-2A" + "(August 2015)" * }
{
[ [{ "validity" * }]
{ "" "" "@" "" "" "" "@" }
}
]
[ [{ "equivalences" * }]
- { "@" "" "@" "" "" "" }
- { "+" "+" "-" "-" "-" "+" }
+ { "@" "" "@" "" "" "" "" }
+ { "+" "+" "-" "-" "-" "+" "+" }
{ "primitive decomposed rt-equivalence (terms)"
"single-step context-sensitive r-eqivalence (terms)"
"primitive context-sensitive r-eqivalence (terms) removed"
"context-free r-eqivalence (terms) removed"
"level equivalence (binary arities) removed"
- "syntactic equivalence (selected lenvs, referred lenvs, selected closures)"
+ "properties with syntactic equivalence (referred lenvs)"
+ "syntactic equivalence (selected lenvs, referred lenvs, referred closures)"
}
]
[ [{ "partial orders" * }]
- { "" "" "" "" "" "" "" }
- { "+" "*" "+" "-" "-" "-" "-" }
+ { "" "" "" "" "" "" "" "" }
+ { "+" "*" "+" "-" "-" "-" "-" "-" }
{ "big-tree order relations (closures)"
- "primitive order relations for closures"
+ "primitive order relations (closures)"
"simple weight (restricted closures)"
+ "order relation (lenvs) based on look-up removed"
"order relation (lists of terms) based on lengths removed"
- "order relations (binary arities) based on weights removed"
+ "order relations (terms, lenvs, binary arities) based on weights removed"
"simple weights (binary arities) removed"
"complex weight (terms) removed"
}
}
]
[ [{ "normal form predicates" * }]
- { "" "" "" "" "" "" "" "" "" }
- { "+" "+" "+" "+" "+" "-" "+" "+" "+" }
+ { "" "" "" "" "" "" "" "" "" "" }
+ { "+" "+" "+" "+" "+" "+" "-" "+" "+" "+" }
{ "evaluation for full rt-reduction (terms)"
+ "evaluation for reduction (terms)"
"normal form for full rt-reduction (terms)"
- "irreducible forms for fulld rt-reduction (terms)"
+ "irreducible forms for full rt-reduction (terms)"
"reducible forms for full rt-reduction (terms)"
"evaluation for reduction (terms)"
"normal form for reduction (lists of terms) removed"
}
]
[ [{ "reduction and type synthesis" * }]
- { "" "" "@" "@" "" "" "" "@" "@" }
- { "+" "+" "+" "*" "-" "+" "-" "*" "-" }
+ { "" "" "@" "@" "" "" "" "" "@" "@" }
+ { "+" "+" "+" "*" "-" "+" "+" "-" "*" "-" }
{ "stratified full rt-computation (terms, lenvs)"
"stratified full rt-transition (terms, lenvs)"
"decomposed rt-computation (terms)"
"primitive counted iterated type synthesis with δ,s,l,e (terms)"
"syntax-oriented type synthesis (terms) removed"
"refinement for reduction (lenvs)"
+ "context-sensitive computation (lenvs)"
"context-free computation (terms) removed"
"primitive context-sensitive transition with typed β, δ, (wrong) ζ, θ, ε (terms, lenvs)"
"context-free transition (terms, lenvs) removed"
}
]
[ [{ "degree" * }]
- { "@" "" "@" "" }
+ { "" "@" "" "@" }
{ "+" "+" "+" "+" }
{ "refinement for degree (lenvs)"
"degree assignment (terms)"
"refinement (selected lenvs)"
"append (lenvs)"
"left cons (lenvs) removed"
- "flat construction clear (lenvs) removed"
+ "flat entry clear (lenvs) removed"
"sort extraction (lenvs) removed"
"context predicate (terms) removed"
"neutral predicate (terms)"
]
[ [{ "parameters" * }]
{ "" "" }
- { "+" "-"}
- { "concrete sort hierarchies"
+ { "+" "-" }
+ { "instances (sort hierarchy)"
"iterated next function (sort hierarchy) removed"
}
]
]
class "red"
- [ { "λδ-1A" + "(November 2006)" * }
+ [ { "λδ-1A" + "(May 2008)" * }
{
[ [{ "validity" * }]
{ "@" "" "" }
}
]
[ [{ "partial orders" * }]
- { "" "" "" "" }
- { "+" "+" "+" "+" }
- { "order relation (specialized lists of terms) based on lengths"
+ { "" "" "" "" "" }
+ { "+" "+" "+" "+" "+" }
+ { "order relation (lenvs) based on look-up"
+ "order relation (specialized lists of terms) based on lengths"
"order relations (terms, lenvs, closures, binary arities) based on weights"
"simple weights (terms, lenvs, closures, binary arities)"
"complex weight (terms)"
[ [{ "normal form predicates" * }]
{ "" }
{ "+" }
- { "normal form for context-sensitive reduction (terms, specialized lists of terms)"
+ { "normal form for reduction (terms, specialized lists of terms)"
}
]
[ [{ "reduction and type synthesis" * }]
}
]
[ [{ "relocation and slicing" * }]
- { "" "" "" "" "" "" "" "" }
- { "+" "+" "+" "+" "+" "+" "+" "+" }
- { "order relation (lenvs) based on look-up"
- "look-up predicate (lenvs)"
+ { "" "" "" "" "" "" "" }
+ { "+" "+" "+" "+" "+" "+" "+" }
+ { "look-up predicate (lenvs)"
"finite slicing (lenvs)"
"basic slicing (lenvs)"
"finite relocation (terms, specialized lists of terms)"
projects / helm.git / blobdiff