Datos Identificativos 2012/13
Asignatura (*) Matemáticas Discretas II Código 614111406
Titulación
Enxeñeiro en Informática
Descriptores Ciclo Período Curso Tipo Créditos
1º e 2º Ciclo 1º cuadrimestre
Cuarto Obrigatoria 5
Idioma
Castelán
Prerrequisitos
Departamento Computación
Coordinación
Alonso Pardo, Miguel angel
Correo electrónico
miguel.alonso@udc.es
Profesorado
Alonso Pardo, Miguel angel
Blanco Ferro, Antonio angel
Gómez Rodríguez, Carlos
Vilares Ferro, Jesus
Correo electrónico
miguel.alonso@udc.es
antonio.blanco.ferro@udc.es
carlos.gomez@udc.es
jesus.vilares@udc.es
Web
Descrición xeral 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)

Competencias do título
Código Competencias da titulación
A3 Concibir e planificar o desenvolvemento de aplicacións informáticas complexas ou con requisitos especiais.
A11 Implantar sistemas de calidade segundo estándares internacionais.
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.

Resultados de aprendizaxe
Competencias de materia (Resultados de aprendizaxe) Competencias da titulación
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
A11
B3
B11
Introducir o lambda-cálculo, tipado e non tipado, como núcleo fundamental das linguaxes de programación. A3
A11
B3
B11
B12
Comprender os fundamentos do subtipado. A3
A11
B3
B11
B15
Coñecer e ser capaz de aplicar certos conceptos básicos da verificación formal. A3
A11
B3
B11
B12
B15

Contidos
Temas Subtemas
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.

Planificación
Metodoloxías / probas Horas presenciais Horas non presenciais / traballo autónomo Horas totais
Sesión maxistral 45 45 90
Prácticas de laboratorio 15 15 30
Proba obxectiva 3 0 3
 
Atención personalizada 2 0 2
 
*Os datos que aparecen na táboa de planificación son de carácter orientativo, considerando a heteroxeneidade do alumnado

Metodoloxías
Metodoloxías Descrición
Sesión maxistral 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.
Prácticas de laboratorio 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.
Proba obxectiva Proba na que se evaluarán os coñecementos adquiridos tanto na parte teórica como a parte práctica da asignatura.

Atención personalizada
Metodoloxías
Proba obxectiva
Descrición
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.

Avaliación
Metodoloxías Descrición Cualificación
Proba obxectiva Dominio dos coñecementos da materia. 80
Prácticas de laboratorio Realización das prácticas. Compresión e análisis crítico de cada unha delas. 20
 
Observacións avaliación

Fontes de información
Bibliografía básica

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.
Bibliografía complementaria
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.

Recomendacións
Materias que se recomenda ter cursado previamente
Programación Funcional/614111635

Materias que se recomenda cursar simultaneamente

Materias que continúan o temario
Matemática Discreta I/614111107
Algoritmos/614111206
Programación Declarativa/614111207

Observacións


(*)A Guía docente é o documento onde se visualiza a proposta académica da UDC. Este documento é público e non se pode modificar, salvo casos excepcionais baixo a revisión do órgano competente dacordo coa normativa vixente que establece o proceso de elaboración de guías