4
$\begingroup$

From what I understand of Normalization by Evaluation (NbE) as a technique to implement conversion, it 1) computes (some representation of) normal forms for each of the terms to compare, and 2) compares those. Usually, when hearing about NbE, you mostly hear about part 1), because this is where most of the things happen. But I was wondering about how 2) is performed in practice.

In particular, in some settings step 1) might compute normal forms that can somewhat differ (that is, not be α-equal). One example is with proof-irrelevant propositions, where you do not want to reduce any strict proposition, as this is not necessary: by virtue of proof-irrelevance, any two propositions are convertible. But then you have to incorporate this irrelevance in step 2). How would this go? Another example is if you try and optimize η-expansion of functions, and rather than always computing η-long normal forms you try and do η-expansion by need in step 2). Are there implementations of NbE that do this, and if so how?

Improve this question
$\endgroup$
5
  • $\begingroup$ From my understanding NbE mostly does not care about reduction steps at all, so "η-expansion" doesn't quite make sense. There is no explicit "step" that applies an η-expansion rule. $\endgroup$
    – Trebor ♦
    Commented Nov 24, 2022 at 16:48
  • $\begingroup$ What I mean is that as far as I understand, naïve NbE computes β-normal η-long forms. Even if not performed by means of reduction, this is still a form of η-expansion! And not triggering needless such η-expansions, be it by reduction or evaluation, is one of the important optimizations of Coq and Agda's conversion-checkers. $\endgroup$
    – Meven Lennon-Bertrand ♦
    Commented Nov 24, 2022 at 17:30
  • $\begingroup$ Typed comparison would help, it seems. $\endgroup$
    – Andrej Bauer
    Commented Nov 24, 2022 at 21:56
  • $\begingroup$ Probably, yes, although in the two cases I mention you can avoid it: for η, you can expand only when you compare a term that is not a λ to one that is; for SProp you need only to maintain/compute the sort of a term and not its type. This is much cheaper because sorts are stable by substitution, so you do not need to compute with them, while in general you need a costly evaluation of types in typed conversion. In practice in Coq, SProp is implemented like this, storing a sort whenever we store a type (variable in a context, return type of pattern-matching…), and then propagating it around. $\endgroup$
    – Meven Lennon-Bertrand ♦
    Commented Nov 25, 2022 at 10:16
  • 4
    $\begingroup$ I'll just buy a faster computer and compute all the types. $\endgroup$
    – Andrej Bauer
    Commented Nov 27, 2022 at 20:19

1 Answer 1

Reset to default
6
$\begingroup$

I will present the conversion procedure that is used in András Kovács' Elaboration zoo and its extension to the η-rule for the unit type. It is based on Coquand's type-checking algorithm.

In Normalization by Evaluation we distinguish between terms and values. There is an evaluation function that evaluates terms into values, and a quoting (or read-back) function that converts values back into terms.

There are multiple ways to implement quoting: it would be possible to quote values into normal forms, but it is preferable to quote values into terms that are as small as possible. In particular we don't want to do unnecessary η-expansions.

Conversion checking is performed at the level of values.

For a type theory with Type : Type, Pi-types, Sigma-types and a unit type, the following representation of values is used (in OCaml):

type value_t
 = Neutral of neutral
 | Type
 | Pi of value_t * closure
 | Lam of value_t (* the domain type *) * closure
 | Sigma of value_t * closure
 | Pair of value_t * value_t
 | Unit 
 | UnitTT

and closure = value_t -> value_t

and neutral 
 = NVar of int (* de Bruijn level *) * value_t (* the type of the variable *) 
 | NApp of neutral * value_t
 | NProj1 of neutral
 | NProj2 of neutral

There may be multiple representations of the same semantic value. For example Pair(UnitTT,UnitTT) and Neutral(NVar(0, Sigma(Unit, fun _ -> Unit))) should be convertible.

With this value representation, the conversion checking procedure needs to handle the following cases:

let rec conv lvl : value_t * value_t -> bool = function
  | Type,Type -> true
  | Pi(a1,b1),Pi(a2,b2) -> __
  | Sigma(a1,b1),Sigma(a2,b2) -> __
  | Unit,Unit -> true

  | Lam(a1,b1), Lam(a2,b2) -> __
  | f1, Lam(a2,b2) -> __
  | Lam(a1,b1), f2 -> __

  | Pair(a1,b1), Pair(a2,b2) -> __
  | p1, Pair(a2,b2) -> __
  | Pair(a1,b1), p2 -> __

  | UnitTT,_ -> true
  | _,UnitTT -> true

  | Neutral(n1),Neutral(n2) -> 
    if is_strict_prop lvl (neutral_type n1) 
    then true
    else conv_neutral lvl n1 n2

  | _,_ -> false (* The values are not convertible. *)

The missing parts __ depend on other elements of the implementation. The corresponding code in the elaboration-zoo can be found here, but it doesn't handle the unit type.

The argument lvl of conv is an integer that has to be greater than any variable occurring in the value. It is used to generate a new variable when checking whether closures are convertible. Alternatively, it is possible to use fresh names.

For Pi-types and Sigma-types, checking the η-rule is done by the cases that compare a lambda or a pair with a neutral value. For the η-rule of the unit type, this is not sufficient, because for example two different variables may be convertible. However the only missing cases involves two neutral values. It suffices to check whether the type is a strict proposition when checking the conversion of two neutral values.

let rec is_strict_prop lvl : value_t -> bool = function
  | Type -> false
  | Unit -> true
  | Pi(a,b) -> is_strict_prop (lvl+1) (b (var lvl a))
  | Sigma(a,b) -> is_strict_prop lvl a && is_strict_prop (lvl+1) (b (var lvl a))
  | Neutral(_) -> false

Conversion assumes that the two values have the same type. However conversion is not type-directed: the common type of the two values is not an argument of conv. Instead every variable is tagged with its type in the representation of values. This provides a way to compute the type of a neutral value when needed. Recomputing the type of a general value is however not possible with this representation.

Improve this answer
$\endgroup$
4
  • 1
    $\begingroup$ Thanks for the answer! Two extra questions: in the non-diagonal cases for Lam and Pair, you know by your typing invariant that f1/f2/p1/p2 must be a Neutral, which is why you did not bother making a more special case, like Neutral n1, Lam(a2,b2)? And in the missing __, when you go under a binder, you do a recursive call with either the closure applied to var lvl a, just like in is_strict_prop, whene there is one, or with the same term (implicitly lifted by one) when you know it must be a neutral? $\endgroup$
    – Meven Lennon-Bertrand ♦
    Commented Nov 30, 2022 at 12:46
  • 1
    $\begingroup$ Also, maybe a more precise link to the actual equivalent of this code in the Elaboration zoo, rather than just the repo, would be very useful to navigate a complete codebase and get a better feeling of what happens. $\endgroup$
    – Meven Lennon-Bertrand ♦
    Commented Nov 30, 2022 at 12:47
  • 1
    $\begingroup$ Yes, for this value representation, f1/f2/p1/p2 is always neutral in the cases that handle eta for Pi/Sigma types. In order to deal with metavariables in unification, we sometimes distinguish between flexible and rigid neutral values, see for instance this type of values. $\endgroup$
    – Rafaël Bocquet
    Commented Nov 30, 2022 at 15:58
  • 1
    $\begingroup$ I have added a link to the one of the conversion functions in the elaboration zoo. It does not correspond exactly to what I presented, but it should show how to fill the missing parts of my answer. $\endgroup$
    – Rafaël Bocquet
    Commented Nov 30, 2022 at 16:01

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.