Identifying Data 2015/16
Subject (*) Matemáticas Discretas II Code 614111406
Study programme
Enxeñeiro en Informática
Descriptors Cycle Period Year Type Credits
First and Second Cycle 1st four-month period
 Fourth Obligatoria 5
Language
Spanish
Teaching method Face-to-face
Prerequisites
Department Computación
Coordinador
Alonso Pardo, Miguel angel
 E-mail
miguel.alonso@udc.es
Lecturers
Alonso Pardo, Miguel angel
 E-mail
miguel.alonso@udc.es
Web
General description En esta asignatura se profundiza en los fundamentos de la computación, con especial énfasis en:
* Combinatoria y recursión (funciones generatrices, relaciones de recurrencia, y su aplicación en el diseño de algoritmos)
* Sistemas de tipos (especificación formal de los sistemas de tipos para conformar la semántica de los lenguajes de programación)
* Prueba de teoremas (introducción práctica a los asistentes de pruebas, tomando la formalización de sistemas de tipos como caso práctico)

Study programme competencies
Code Study programme competences / results
A3 Concibir e planificar o desenvolvemento de aplicacións informáticas complexas ou con requisitos especiais.
B2 Resolver problemas de forma efectiva.
B3 Aplicar un pensamento crítico, lóxico e creativo.
B11 Razoamento crítico.
B12 Capacidade para a análise e a síntese.
B15 Motivación pola calidade.

Learning aims
Learning outcomes Study programme competences / results
Manexar conceptos de combinatoria, fundamentalmente as funcións xeratrices. B3
B11
B12
Aprender a resolver relacións de recurrencia e as suas aplicacións ao estudo da complexidade dos algoritmos. B2
B11
Comprender os conceptos básicos dos sistemas de tipos. A3
 B3
B11
Introducir o lambda-cálculo, tipado e non tipado, como núcleo fundamental das linguaxes de programación. A3
 B3
B11
B12
Comprender os fundamentos do subtipado. A3
 B3
B11
B15
Coñecer e ser capaz de aplicar certos conceptos básicos da verificación formal. A3
 B2
B3
B11
B12
B15

Contents
Topic Sub-topic
Parte I: Combinatoria e recursión.
 1.1 Funcións xeratrices ordinarias.
1.2 Funcións xeratrices exponenciais.
1.3 Relacións de recurrencia lineais homoxéneas.
1.4 Relacións de recurrencia lineais non homoxéneas.
1.5 Aplicacións a algoritmos.
Parte II: Sistemas de tipos 2.1 Introducción.
2.2 Sistemas non tipados.
2.3 Tipos simples.
2.4 Subtipado.
Parte III: Prueba de teoremas 3.1 Introducción al sistema de prueba de teoremas Coq.
3.2 Prueba de teoremas sencillos en Coq.

Planning
Methodologies / tests Competencies / Results Teaching hours (in-person & virtual) Student’s personal work hours Total hours
Guest lecture / keynote speech A3 B2 B3 B11 B15 45 45 90
Laboratory practice B2 B12 B15 15 15 30
Objective test A3 B2 B3 B11 B12 3 0 3
 
Personalized attention 2 0 2
 
(*)The information in the planning table is for guidance only and does not take into account the heterogeneity of the students.

Methodologies
Methodologies Description
Guest lecture / keynote speech Exposición oral complementada co uso de medios audiovisuais e a formulación de preguntas dirixidas a os estudantes, co obxetivo de transmitir coñecemento así como de estimular o razoamento crítico do estudiante.
Laboratory practice Actividade que permite que os estudantes aprendan efectivamente a través da realización de actividades de
carácter práctico, neste caso, prácticas, demostracions e exercicios.
Objective test Proba na que se evaluarán os coñecementos adquiridos tanto na parte teórica como a parte práctica da asignatura.

Personalized attention
Methodologies
Objective test
Description
Os alumnos disporán de atención persoalizada no horario de titorías establecido, para resolver dudas xerais da asignatura. Estas titorías realizaranse tanto no despacho do profesor como a través do foro virtual.

Assessment
Methodologies Competencies / Results Description Qualification
Objective test A3 B2 B3 B11 B12 Dominio dos coñecementos da materia. 80
Laboratory practice B2 B12 B15 Realización das prácticas. Compresión e análisis crítico de cada unha delas. 20
 
Assessment comments

En el caso de nuevos alumnos, al no haber horario de laboratorios asignados a la asignatura, la calificación de la asignatura se basara en la nota obtenida en el examen, que incluye dos partes teóricas:
* sistemas de tipos
* combinatoria

 y una parte de prácticas:
* demostración automática de teoremas (Coq).

Aquellas prácticas que hayan sido entregadas satisfactoriamente en el curso 2012/13 o anteriores serán tenidas en cuenta.

Para aprobar la asignatura es preciso obtener una nota mínima en cada una de las tres partes que será comunicada a través del Moodle antes de cada convocatoria.

Sources of information
Basic

R. P. Grimaldi. Matemáticas discretas y combinatoria. Addison-Wesley Iberoamericana. Tercera Edición.

B. C. Pierce. Types and Programming Languages. The MIT Press. 2002.

Y. Bertot y P. Casteran. Interactive Theorem Proving and Program Development. Springer. 1998.
Complementary 
R. L. Graham, D. E. Knuth y O. Patashnik. Concrete Mathematics, a foundation for computer science. Addison-Wesley.

K. H. Rosen. Matemática Discreta. McGraw-Hill. Quinta Edición.

J. C. Mitchell. Foundations for programming Languages. MIT Press.

Recommendations
Subjects that it is recommended to have taken before
Matemática Discreta I/614111107
Algoritmos/614111206
Programación Declarativa/614111207

Subjects that are recommended to be taken simultaneously

Subjects that continue the syllabus
Programación Funcional/614111635

Other comments


(*)The teaching guide is the document in which the URV publishes the information about all its courses. It is a public document and cannot be modified. Only in exceptional cases can it be revised by the competent agent or duly revised so that it is in line with current legislation.