7
$\begingroup$

Administrative normal form is a program intermediate representation in which each immediate instruction has a name. It is used in GHC and OCaml.

K-normalized form is an intermediate representation in which each instruction consists of one assignment and operation. It's used in MLKit, Min-Caml, and GoCaml.

Both A-normalization and K-normalization involve generating a let expression with a continuation.

A-normalization and K-normalization seem to be exactly the same transformation. What is the difference between them such that they deserve different names?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
3
$\begingroup$

As far as my search-foo led me; K-Normal Form is inspired by A-Normal Form, but instrumented for use in Storage Mode Analysis, which is a static program analysis used for inferring memory mangement directives for functional programs.

The term seems to originate from the following publication: L. Birkedal, M. Tofte, and M. Vejlstrup. From region inference to von Neumann machines via region representation inference.

A copy of the publication can at the time of writing be obtained from L.Birkedal's faculty webpage under publications.

Improve this answer
$\endgroup$
3
  • 2
    $\begingroup$ While the origin of the term is interesting, I don't directly see how this explains a difference. Could you clarify what exactly the difference is between the two normalization procedures? (if any?) $\endgroup$
    – Discrete lizard ♦
    May 16, 2019 at 9:49
  • 1
    $\begingroup$ According to the paper (cs.cmu.edu/afs/cs/user/birkedal/pub/rri-popl96.ps.gz), K-normal form binds each intermediate expression to a variable, but does not linearize the let-bindings because doing so would impede region inference. $\endgroup$
    – Del
    May 29, 2019 at 21:59
  • 1
    $\begingroup$ I didn't update the answer yet since my current understanding is that linearizing let-bindings is not part of the definition of ANF, so I am not sure if this is a difference. Another possible difference mention in the paper is that the terms must be typed, but if this is only ment in regards to the type system given in the paper, is also not clear to me. $\endgroup$
    – soren-n
    May 31, 2019 at 2:25

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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