1st Encounter - 19/5/2012 - Introducción

A programming language has the following elements:

  • Syntax (Abstract): "The sequence of symbols that makes up a valid program"
  • Operational Semantics: "Relates a program with what it does"
    -> Asociated to evaluation
  • Implementing: Build a Parser and Build an interpreter / evaluator
  • Type checking
  • Property demonstration

Term:
A program is a term.

double x = x + x

When we evaluate

double 2

[double 2] is the evaluated term

Value:
Subset of terms. When we finish reducing a term, we get one of these.

Example of a language

As a first example, we start defining a language for manipulating booleans elements. This language will have the two boolean values true and false and an if-then-else expression.

The syntax of our language is the following:
T ::= true | false | if T then T else V <- "Terms"
V ::= true | false                  <- "Values"

We can build several valid programs using this language, such as for example:
  • true
  • if true then false else true
  • if true then if false then false else false else false
  • if if true then true else true then true else false

Note: The "metavariables" T and V cannot appear in our program.

Defining the Operational Semantics

We will work with a "smallstep" semantic. That is, we advance by small steps.

Reduction rules systems:

E-IFTRUE: _________________________

                     if true then T1 else T2 -> T1

  • ( -> ): Reduces exactly in 1 step
  • (->>): Reduces in 0 or more steps
  • (-+>): Reduces in 1 or more steps

     

E-IFFALSE: _________________________

                     if false then T1 else T2 -> T2

        All the programs we evaluated before reduce to:
            
                > true

This program cannot be reduced: it does not match any reduce rules. This kind of terms are called "normal forms".
In a well formed program, the normal forms are the values.
              if true then false else true    [E-IFTRUE]
____________________________

false
              if true then if false then false else false else false    [E-IFTRUE]
______________________________________________________

             if false then false else false    [E-IFFALSE]
________________________________

false

> if if true then true else true then true else false

Opa! Esto no matchea con ninguna regla.
Por lo tanto mi lenguaje tiene formas normales que no son valores.
Tengo que agregár más sistemas de reglas de reducción.

T1 -> T1'
E-IF: _______________________________________________

      if T1 then T2 else T3 -> if T1' then T2 else T3

Ahora sí:

                   if if true then true else true then true else false    [E-IF]
___________________________________________________

              if true then true else false    [E-IFTRUE]
____________________________

true

Adding Numbers to Our Language


Sintaxis:

T  := ... | 0 | succ T | pred T | isZero T
V  := ... | NV
NV := 0 | succ NV <- "Valores Numéricos"

Semántica:

R1:
________________

isZero 0 -> true


R2:
_________________________

isZero (succ NV) -> false


R3:
T -> T'
_________________________

isZero (T) -> isZero(T')


R4:
____________________

pred (succ NV) -> NV


R5:
____________________

pred (0) -> 0


R6:
T -> T'
_____________________

pred (T) -> pred (T')


R7:
T -> T'
_____________________

succ (T) -> succ (T')

Hay que notar que ahora, un termino como:

pred (false)

es una forma normal, dado que no puede reducirse.
Es lo que se llama un "Programa Erroneo".

Actividades sugeridas
  • Finalizar la implementación incluyendo booleanos y enteros.
  • Asociar un número a cada valor para poder identificar cada una de sus apariciones univocamente al reducirlo. Por ejemplo:

    if false1 then true1 else true2 -> true2

  • Cambiar el eval para que se imprima cada regla por la que se pasa (en lugar de solo mostrar cada step). Ej:
if (if (if true then true else false) then true else false) then true else false
________________________________________________________________________________

if (if true then true else false) then true else false
______________________________________________________

if true then true else false
____________________________

true

  • En el primer paso el evaluador "se mete" en la condición, dejando suspendido el if más externo. Lo más fácil sería intentarlo sobre los booleanos, pero podría hacerse también contemplando los números.
    • En el segundo paso da un paso de evaluación en la condición (que a su vez podría implicar más mini-pasos, en caso de que haya que usar E-IF nuevamente).
    • En el tercer paso se recupera el contexto y se llega al resultado original de E-IF.
    • Proponer otra semántica operacional en la que aplicar la regla de E-IF conste de tres pasos:
  • Extender el lenguaje B para contemplar not, and y or.
  • Extender el lenguaje BN para contemplar también a los enteros. En este lenguaje tenemos dos formas normales: succn(0) y predn(0).
    ¿Se pueden definir las reglas de evaluación de forma que este lenguaje no sea ambiguo?

Lecturas sugeridas


Ċ
Guillermo Polito,
May 21, 2012, 9:32 PM
ċ
Taller de Lenguajes - Clase 01.hs
(1k)
Guillermo Polito,
May 21, 2012, 9:22 PM
ċ
lenguajeBool-complicado.hs
(1k)
Guillermo Polito,
May 21, 2012, 9:22 PM
ċ
lenguajeBool.hs
(1k)
Guillermo Polito,
May 21, 2012, 9:22 PM
Comments