Can we avoid neutral terms for built-ins?

[jaccokrijnen]

This would simplify the dynamic semantics. Neutral terms are necessary because of built-in functions. Perhaps we could hypothesize that all built-ins have a valid implementation:

⟦⋅⟧ : Builtin τ -> Term τ

And add:

  ⟦B⟧ =[j]=> v
  ------------- E-Builtin
   B  =[j]=> v

Question is: is it a sensible axiom/assumption? Can all built-ins be expressed within Fωμ? Consider

• sha_256: this might be complicated to implement (but in principle, possible)

  • if there exists a pure haskell implementation, we could obtain the term by running the compiler?

• if_then_else: it has to be lazy in its branches (e.g. Error)

  Is if_then_else it actually lazy? No it is not, Haskell if-then-else gets translated to case distinction, which is compiled into "lazy" branches.

  some uplc tests: https://github.com/input-output-hk/plutus/blob/510812298d4359783722512bed2f522c630969a8/plutus-ledger-api/test/Spec/Eval.hs

  2021 PLC spec (section 6): https://hydra.iohk.io/build/17026172/download/1/plutus-core-specification.pdf

[jaccokrijnen]

Manuel suggested that

⟦⋅⟧ : Builtin τ -> Term τ

Can be implemented with η-expansion, i.e.:

⟦b⟧ = (\x ... z -> b x ... z)

I think this would still require an evaluation rule for fully-applied built-ins

[jaccokrijnen]

Currently, we have BuiltinMeanings.compute_defaultfun, which interprets (most but not all) fully-applied built-ins, and

  | E_NeutralApplyFull: forall nv1 v2 v,
      fully_applied (Apply nv1 v2) -> 
      compute_defaultfun (Apply nv1 v2) = Datatypes.Some v ->
      Apply nv1 v2 =[1]=> v
  | E_NeutralTyInstFull: forall nv1 v T,
      fully_applied (TyInst nv1 T) -> 
      compute_defaultfun (TyInst nv1 T) = Datatypes.Some v ->                                                                                                                                                      
      TyInst nv1 T =[1]=> v

[jaccokrijnen]

A simpler way would be to represent built-ins as always fully applied, and eta expand when converting haskell AST to coq AST.

For example:

BuiltIn AddInteger ======> \x. \y. BuiltIn AddInteger [x, y]

Michael didn't see any problems with representing built-ins in Coq this way. Except if we are interesting in costing, which we are not.