Greg Exercise 02 - bound names, other grammars

[Jake-Gillberg]

Give the domain equation and the scala (or haskell) representations for the grammars of:

• blue calculus
• ambient process calculus
• (extra credit) linear lambda calculus

Add the definitions free and bound names to the scala (or haskell) representation of rho calculus

[Jake-Gillberg]

https://gist.github.com/Jake-Gillberg/c661903026c0616acebeb8ec93e47db3

[golovach-ivan]

@Jake-Gillberg I think you variant is not fully correct.

Meredith, Radestock, 2005, "A Reflective Higher-order Calculus":

We now come to one of the first real subtleties of this calculus. Both the calculation of the free names of a process and the determination of structural congruence between processes critically depend on being able to establish whether two names are equal.

So FN MUST use name equality ≡_N in set operations ('∪' and '\'), not implicitly standard case classes equality (in Scala Set operations ('+', '-', '|', '&~')).

Let P = for(\@0 <- \@(\@0!(0))).((for(\@0 <- \@(0|0)).0)

FN(P) = {@(\@0!(0))} ∪ (FN(for(\@0 <- \@(0|0)).0) \ {\@0}) = {@(\@0!(0))} ∪ (FN(\@(0|0))) \ {\@0}) = {@(\@0!(0))} ∪ ( {\@(0|0)} \ {\@0} ) = and = {@(\@0!(0))} ∪ ( {\@0} \ {\@0} ) = {@(\@0!(0))} ∪ {} = {@(\@0!(0))} NOT = {@(\@0!(0))} ∪ {\@(0|0)} = {@(\@0!(0))} ∪ {\@(0|0)} = {@(\@0!(0)), \@(0|0)}

P.S. Because \@(0|0) ≡_N \@0

[Jake-Gillberg]

@golovach-ivan Ah, yup! You are totally correct, thanks! I have a definition of name equality and structural equality working in scala here, but I don't preserve the structure of bound names, so it would be difficult to implement the Free and Bound name definitions without some modifications.

[golovach-ivan]

@Jake-Gillberg About Scala code style (IMHO): 1) please, add usage example

2) if method mody is one expression - do not use curve brackets (lines: 31+38, 42+48, 68+73, etc)

// not
    override def equals(other: Any): Boolean = {
      other match {
        case that: Quote => p == that.p
        case _ => false
      }
    }
// but
    override def equals(other: Any): Boolean = other match {
      case that: Quote => p == that.p
      case _ => false
    }

// not
    override val hashCode: Int = {
      41 + p.hashCode
    }
// but
    override val hashCode: Int = 41 + p.hashCode

3) with tuple members you can use assigning to pattern with named vals in for-comprehension (hard to understand this: if input._1._1 == lift._1._1)

  val p = for (
    (name, age, (_, houseNum)) <- Seq(("Mike", 42, ("StreetA", "house#1")), ("Anna", 25, ("StreetA", "house#1")))
  ) yield name

4) place something and compation object for it - together

private final type FreqMap[X] = Map[X, Int]
private final object FreqMap {
  def empty[X] = Map.empty[X, Int]
}

5) class without body does not need empty curve brackets

// not
  final class Drop( x: Name ) extends Process( inputs = FreqMap.empty[(Name, Process)],
                                               lifts = FreqMap.empty[(Name, Process)],
                                               drops = Map(x -> 1),
                                               height = 0 ) {
  }
// but
  final class Drop( x: Name ) extends Process( inputs = FreqMap.empty[(Name, Process)],
                                               lifts = FreqMap.empty[(Name, Process)],
                                               drops = Map(x -> 1),
                                               height = 0 ) 

6) use type params inference

// not
  final object Zero extends Process(
    inputs = FreqMap.empty[(Name, Process)],
    lifts = FreqMap.empty[(Name, Process)],
    drops = FreqMap.empty[Name],
    height = 0)
// but
  final object Zero extends Process(
    inputs = FreqMap.empty,
    lifts = FreqMap.empty,
    drops = FreqMap.empty,
    height = 0)

7) Move constructors default values from children to parent (maybe?)

  sealed class Process(val inputs: Inputs = FreqMap.empty,
                                   val lifts: Lifts = FreqMap.empty,
                                   val drops: Drops = FreqMap.empty,
                                   val height: Int = 0)

  final object Zero extends Process

  final class Drop(x: Name) extends Process(drops = Map(x -> 1))

  final class Parallel(p: Process, q: Process) extends Process(
    inputs = mergeMaps(Seq(p.inputs, q.inputs)),
    lifts = mergeMaps(Seq(p.lifts, q.lifts)),
    drops = mergeMaps(Seq(p.drops, q.drops)),
    height = math.max(p.height, q.height))

  final class Lift(x: Name, p: Process) extends Process(
    lifts = Map((x, p) -> 1),
    height = p.height)

  final class Input(y: Name, x: Name, p: Process) extends Process(
    inputs = Map((x, substitute(y, BoundName(p.height), p)) -> 1),
    height = p.height + 1)

8) from math point of view (in my opinion) you do not need '41 +' here

// not
    override val hashCode: Int = {
      41 + p.hashCode
    }
// but
    override val hashCode: Int = p.hashCode

9) it can be more consistent to use FreqMap constructor not Map

// not
  final class Drop( x: Name ) extends Process( inputs = FreqMap.empty[(Name, Process)],
                                               lifts = FreqMap.empty[(Name, Process)],
                                               drops = Map(x -> 1), // <<<=== HERE
                                               height = 0 ) {
  }
// but
  final class Drop( x: Name ) extends Process( inputs = FreqMap.empty[(Name, Process)],
                                               lifts = FreqMap.empty[(Name, Process)],
                                               drops = FreqMap(x -> 1),
                                               height = 0 ) {
  }
  private final object FreqMap {
    ...
    def apply[X, B](elems: (X, Int)*): FreqMap[X] = Map[X, Int](elems: _*)
  }

10) personally i like

// this
object FreqMap {
  def apply[X] = Map.empty[X, Int]
}
val x: FreqMap[String] = FreqMap()
val y: Seq[Int] = Seq()

// not this
object FreqMap {
  def empty[X] = Map.empty[X, Int]
}
val x: FreqMap[String] = FreqMap.empty()
val y: Seq[Int] = Seq.empty()

[kayvank]

@Jake-Gillberg I finally caught up with Greg's lectures & am trying to catch up with the HW now. Here is my take on the 1st HW, FreeName computations. https://github.com/kayvank/calculi

[kayvank]

@Jake-Gillberg Here my take on the Arabic-numerals assignment: https://github.com/kayvank/arabic-numerals

[kayvank]

A few category theory resources:

• Bartosz Milesski, https://bartoszmilewski.com/, here is a link to his book: https://github.com/hmemcpy/milewski-ctfp-pdf

• Mike Stay presentation: https://www.youtube.com/watch?v=rZawYtTdObo